{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T18:10:50Z","timestamp":1726251050163},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540502418"},{"type":"electronic","value":"9783540459606"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50241-6_33","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:18:57Z","timestamp":1330201137000},"page":"118-128","source":"Crossref","is-referenced-by-count":11,"title":["Induction in the elementary theory of types and names"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"J\u00e4ger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M.J. Beeson","year":"1985","unstructured":"M.J. Beeson, Foundations of Constructive Mathematics, Springer, Berlin, 1985."},{"key":"9_CR2","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0091894","volume-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies","author":"W. Buchholz","year":"1981","unstructured":"W. Buchholz, S. Feferman, W. Pohlers, W. Sieg, Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Lecture Notes in Mathematics 897, Springer, Berlin, 1981."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"L. Cardelli and P. Wegner, On understanding types, data abstraction and polymorphism, Computing surveys 17 (1985).","DOI":"10.1145\/6041.6042"},{"key":"9_CR4","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki and S.F. Smith, Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings EUROCAL 85","author":"T. Coquand","year":"1985","unstructured":"Th. Coquand and G. Huet, Constructions: A higher order proof system for mechanizing mathematics, in: Proceedings EUROCAL 85, Lecture Notes in Computer Science 203, Springer, Berlin, 1985."},{"key":"9_CR6","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"N.G. de Bruijn, A survey of AUTOMATH, in: J.P. Seldin and J.R. Hindley (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, New York, 1980."},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner and C. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science 78, Springer, Berlin, 1979."},{"key":"9_CR8","series-title":"Lecture Notes in Mathematics","volume-title":"Algebra and Logic","author":"S. Feferman","year":"1975","unstructured":"S. Feferman, A language and axiom for explicit mathematics, in: Algebra and Logic, Lecture Notes in Mathematics 450, Springer, Berlin, 1975."},{"key":"9_CR9","volume-title":"Handbook of Mathematical Logic","author":"S. Feferman","year":"1977","unstructured":"S. Feferman, Theories of finite type, in: J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977."},{"key":"9_CR10","volume-title":"Proceedings of Logic Colloquium '78","author":"S. Feferman","year":"1979","unstructured":"S. Feferman, Constructive theories of functions and classes, in: M. Boffa, D. van Dalen, K. McAloon (eds.), Proceedings of Logic Colloquium '78, North-Holland, Amsterdam, 1979."},{"key":"9_CR11","volume-title":"The Patras Symposium","author":"S. Feferman","year":"1982","unstructured":"S. Feferman, Iterated fixed-point theories: application to Hancock's conjecture, in: G. Metakides (ed.), The Patras Symposium, North-Holland, Amsterdam, 1982."},{"key":"9_CR12","unstructured":"S. Feferman, A theory of variable types, Revista Colombiana de Mathem\u00e1ticas, XIX, (1985)."},{"key":"9_CR13","unstructured":"S. Feferman, Weyl vindicated: \u201dDas Kontinuum\u201d 70 years later, Preprint, Stanford, 1987."},{"key":"9_CR14","unstructured":"S. Feferman, The polymorphic typed \u03bb-calculus (and all that) in a type-free axiomatic framework, Preprint, Stanford, 1988."},{"key":"9_CR15","volume-title":"Proceedings 2nd Scandinavian Logic Symposium","author":"J.-Y. Girard","year":"1971","unstructured":"J.-Y. Girard, Une extension de l'interpretation de G\u00f6del a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types, in: Proceedings 2nd Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard, The system F of variable types, fifeteen years later, Theoretical Computer Science 45 (1986).","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"9_CR17","unstructured":"S. Hayashi and H. Nakano, PX a computational logic, Report Research Institute for Mathematical Sciences, Kyoto University, Kyoto, 1987."},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of TAPSOFT '87","author":"G. Huet","year":"1987","unstructured":"G. Huet, Induction principles formalized in the calculus of constructions, in: H. Ehrig, R. Kowalski, G. Levi and U. Montanari (eds.), Proceedings of TAPSOFT '87, Lecture Notes in Computer Science 249, Springer, Berlin, 1987."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"G. J\u00e4ger, Type theory and explicit mathematics, in: Proceedings of Logic Colloquium '87, to appear.","DOI":"10.1016\/S0049-237X(08)70127-7"},{"key":"9_CR20","volume-title":"Proceedings 6th International Congress for Logic, Methodology and Philosophy of Science","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"P. Martin-L\u00f6f, Constructive mathematics and computer programming, in: Proceedings 6th International Congress for Logic, Methodology and Philosophy of Science, North-Holland, Amsterdam, 1982."},{"key":"9_CR21","volume-title":"Elementary Induction on Abstract Structures","author":"Y.N. Moschovakis","year":"1974","unstructured":"Y.N. Moschovakis, Elementary Induction on Abstract Structures, North-Holland, Amsterdam, 1974."},{"key":"9_CR22","volume-title":"Proceedings IFIP '83","author":"B. Nordstrom","year":"1983","unstructured":"B. Nordstrom and K. Petersson, Types and specifications, in: Proceedings IFIP '83, North-Holland, Amsterdam, 1983."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"B. Nordstrom and J. Smith, Propositions, types, and specifications in Martin-L\u00f6f's type theory, BIT 24, n. 3 (1984).","DOI":"10.1007\/BF02136027"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings Colloque sur la Programmation","author":"J.C. Reynolds","year":"1974","unstructured":"J.C. Reynolds, Towards a theory of type structure, in: Proceedings Colloque sur la Programmation, Lecture Notes in Computer Science 19, Springer, Berlin, 1974."}],"container-title":["Lecture Notes in Computer Science","CSL '87"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50241-6_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:42Z","timestamp":1605647862000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50241-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540502418","9783540459606"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-50241-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}