{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:41Z","timestamp":1761597041040},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678953"},{"type":"electronic","value":"9783540446224"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44622-2_24","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:32:38Z","timestamp":1187253158000},"page":"356-370","source":"Crossref","is-referenced-by-count":3,"title":["A Theory of Explicit Mathematics Equivalent to ID 1"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Kahle","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Studer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,22]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Luca Cardelli. A Theory of Objects. Springer, 1996.","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"24_CR2","series-title":"Ergebnisse der Mathematik und ihrer Grenzgebiete","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M. Beeson","year":"1985","unstructured":"Michael Beeson. Foundations of Constructive Mathematics. Ergebnisse der Mathematik und ihrer Grenzgebiete; 3.Folge, Bd. 6. Springer, Berlin, 1985."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical studies, volume 897 of Lecture Notes in Mathematics. Springer-Verlag, 1981.","DOI":"10.1007\/BFb0091894"},{"key":"24_CR4","unstructured":"Andrea Cantini. Logical Frameworks for Truth and Abstraction, volume 135 of Studies in Logic and the Foundations of Mathematics.North-Holland, 1996."},{"key":"24_CR5","first-page":"303","volume-title":"Intuitionismus and Proof Theory","author":"S. Feferman","year":"1970","unstructured":"Solomon Feferman. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In A. Kino, J. Myhill, and R. Vesley, editors, Intuitionismus and Proof Theory, pages 303\u2013326. North Holland, Amsterdam, 1970."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Solomon Feferman. A language and axioms for explicit mathematics. In J. Crossley, editor, Algebra and Logic, volume 450 of Lecture Notes in Mathematics, pages 87\u2013139. Springer, 1975.","DOI":"10.1007\/BFb0062852"},{"key":"24_CR7","first-page":"159","volume-title":"Logic Colloquium 78","author":"S. Feferman","year":"1979","unstructured":"Solomon Feferman. Constructive theories of functions and classes. In M. Boffa, D. van Dalen, and K. McAloon, editors, Logic Colloquium 78, pages 159\u2013224. North-Holland, Amsterdam, 1979."},{"issue":"2","key":"24_CR8","doi-asserted-by":"publisher","first-page":"364","DOI":"10.2307\/2274509","volume":"53","author":"S. Feferman","year":"1988","unstructured":"Solomon Feferman. Hilbert\u2019s program relativized: Proof-theoretical and foundational reductions. Journal of Symbolic Logic, 53(2):364\u2013384, 1988.","journal-title":"Journal of Symbolic Logic"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Solomon Feferman. Polymorphic typed lambda-calculus in a type-free axiomatic framework. In W. Sieg, editor, Logic and Computation, volume 106 of Contemporary Mathematics, pages 101\u2013136. American Mathematical Society, 1990.","DOI":"10.1090\/conm\/106\/1057818"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Solomon Feferman. Logics for termination and correctness of functional programs. In Y. Moschovakis, editor, Logic from Computer Sciences, pages 95\u2013127. Springer, 1991.","DOI":"10.1007\/978-1-4612-2822-6_5"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Solomon Feferman. Logics for termination and correctness of functional programs II: Logics of strength PRA. In P. Aczel, H. Simmons, and S.S. Wainer, editors, Proof Theory, pages 195\u2013225. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511896262.009"},{"key":"24_CR12","unstructured":"Solomon Feferman. Does reductive proof theory have a viable rationale? Erkenntnis, 200x.To appear."},{"issue":"3","key":"24_CR13","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0168-0072(93)90013-4","volume":"65","author":"S. Feferman","year":"1993","unstructured":"Solomon Feferman and Gerhard J\u00e4ger. Systems of explicit mathematics with non-constructive \u03bc-operator.P art I. Annals of Pure and Applied Logic, 65(3):243\u2013263, 1993.","journal-title":"Annals of Pure and Applied Logic"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0168-0072(95)00028-3","volume":"79","author":"S. Feferman","year":"1996","unstructured":"Solomon Feferman and Gerhard J\u00e4ger. Systems of explicit mathematics with non-constructive \u03bc-operator. Part II. Annals of Pure and Applied Logic, 79:37\u201352, 1996.","journal-title":"Annals of Pure and Applied Logic"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF01278464","volume":"33","author":"E. Griffor","year":"1994","unstructured":"Ed Griffor and Michael Rathjen. The strength of some Martin-L\u00f6f type theories. Archive for Mathematical Logic, 33:347\u2013385, 1994.","journal-title":"Archive for Mathematical Logic"},{"key":"24_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/3-540-50241-6_33","volume-title":"Computer Science Logic\u2019 87","author":"G. J\u00e4ger","year":"1988","unstructured":"Gerhard J\u00e4ger. Induction in the elementary theory of types and names. In E. B\u00f6rger, H. Kleine B\u00fcning, and M.M. Richter, editors, Computer Science Logic\u2019 87, volume 329 of Lecture Notes in Computer Science, pages 118\u2013128. Springer, 1988."},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Gerhard J\u00e4ger, Reinhard Kahle, and Thomas Strahm. On applicative theories. In A. Cantini, E. Casari, and P. Minari, editors, Logic and Foundation of Mathematics, pages 83\u201392. Kluwer, 1999.","DOI":"10.1007\/978-94-017-2109-7_6"},{"key":"24_CR18","unstructured":"Gerhard J\u00e4ger, Reinhard Kahle, and Thomas Studer. Universes in explicit mathematics.200x.Submitted."},{"key":"24_CR19","unstructured":"Georg Kreisel. Generalized inductive definitions. T echnical report, Stanford Report, 1963."},{"key":"24_CR20","unstructured":"Markus Marzetta. Predicative Theories of Types and Names. Dissertation, Universit\u00e4t Bern, Institut f\u00fcr Informatik und angewandte Mathematik, 1994."},{"key":"24_CR21","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s001530050105","volume":"37","author":"M. Marzetta","year":"1998","unstructured":"Markus Marzetta and Thomas Strahm. The \u03bc quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals. Archive for Mathematical Logic, 37:391\u2013413, 1998.","journal-title":"Archive for Mathematical Logic"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Erik Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory, pages 191\u2013204. Oxford University Press, 1998.","DOI":"10.1093\/oso\/9780198501275.003.0012"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Wolfram Pohlers. Proof Theory, volume 1407 of Lecture Notes in Mathematics. Springer, 1989.","DOI":"10.1007\/978-3-540-46825-7"},{"key":"24_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-63172-0_54","volume-title":"Computer Science Logic CSL\u2019 96: Selected Papers","author":"R. St\u00e4rk","year":"1997","unstructured":"Robert St\u00e4rk. Call-by-value, call-by-name and the logic of values.In D. van Dalen and M. Bezem, editors, Computer Science Logic CSL\u2019 96: Selected Papers, volume 1258 of Lecture Notes in Computer Science, pages 431\u2013445. Springer, 1997."},{"issue":"2","key":"24_CR25","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0956796898002974","volume":"8","author":"R. St\u00e4rk","year":"1998","unstructured":"Robert St\u00e4rk. Why the constant \u2018unde.ned\u2019? Logics of partial terms for strict and non-strict functional programming languages. Journal of Functional Programming, 8(2):97\u2013129, 1998.","journal-title":"Journal of Functional Programming"},{"key":"24_CR26","unstructured":"Thomas Studer. A semantics for \u03bbstr 1 a calculus with overloading and latebinding. Journal of Logic and Computation, 200x.T o appear."},{"key":"24_CR27","unstructured":"Anne Troelstra and Dirk van Dalen. Constructivism in Mathematics, volume II.North Holland, Amsterdam, 1988."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44622-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T21:54:40Z","timestamp":1629582880000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44622-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678953","9783540446224"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-44622-2_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}