{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:29:04Z","timestamp":1761596944243},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037105","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"163-178","source":"Crossref","is-referenced-by-count":14,"title":["The conservation theorem revisited"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Groote","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"H.P. Barendregt. The lambda calculus, its syntax and semantics. North-Holland, revised edition, 1984."},{"issue":"2","key":"12_CR2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H.P. Barendregt","year":"1991","unstructured":"H.P. Barendregt. Introduction to Generalised Type Systems. Journal of Functional Programming, 1(2):125\u2013154, 1991.","journal-title":"Journal of Functional Programming"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"H.P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbai, and T. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"12_CR4","unstructured":"Th. Coquand. Metamathematical investigations of a calculus of constructions. In P. Odifreddi, editor, Logic and Computer Science, pages 91\u2013122. Academic Press, 1990."},{"key":"12_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn. Lambda calculus notations with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem. Indigationes Mathematicae, 34:381\u2013392, 1972.","journal-title":"Indigationes Mathematicae"},{"key":"12_CR6","unstructured":"N.G. de Bruijn. A survey of the project Automath. In J.P. Seldin and J.R. Hindley, editors, to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 579\u2013606. Academic Press, 1980."},{"key":"12_CR7","unstructured":"Ph. de Groote. D\u00e9finition et Propri\u00e9t\u00e9s d'un m\u00e9tacalcul de repr\u00e9sentation de th\u00e9ories. PhD thesis, Universit\u00e9 Catholique de Louvain, Unit\u00e9 d'Informatique, 1991."},{"key":"12_CR8","unstructured":"J.H. Gallier. On Girard's \u201cCandidats de R\u00e9ductibilit\u00e9\u201d. In P. Odifreddi, editor, Logic and Computer Science, pages 123\u2013203. Academic Press, 1990."},{"key":"12_CR9","unstructured":"R.O. Gandy. Au early proof of normalization by A.M. Turing. In J. P. Seldin and J. R. Hindley, editors, to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 453\u2013455. Academic Press, 1980."},{"key":"12_CR10","unstructured":"R.O. Gandy. Proofs of strong normalization. In J. P. Seldin and J. R. Hindley, editors, to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457\u2013478. Academic Press, 1980."},{"issue":"2","key":"12_CR11","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.-J. Ncderhof. Modular proof of strong normalization for the calculus of construction. Journal of Functional Programming, 1(2):155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"12_CR12","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.-Y. Girard","year":"1986","unstructured":"J.-Y. Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159\u2013192, 1986.","journal-title":"Theoretical Computer Science"},{"key":"12_CR13","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"12_CR14","unstructured":"R. Harper, F. Housel, and G. Plotkin. A framework for defining logics. In Proceedings of the second annual IEEE symposium on logic in computer science, pages 194\u2013204, 1987."},{"key":"12_CR15","unstructured":"J.R. Hindley and J.P. Seldin. Introduction to combinators and \u03bb-calculus. London Mathematical Society Student Texts. Cambridge University Press, 1986."},{"key":"12_CR16","series-title":"Mathematical Centre Tracts Nr. 127","volume-title":"PhD thesis","author":"J.W. Klop","year":"1980","unstructured":"J.W. Klop. Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, Mathematical Centre Tracts Nr. 127, 1980."},{"key":"12_CR17","unstructured":"R.P. Nederpelt. Strong normalization in a typed lambda calculus with lambda structured types. PhD thesis, Technische hogeschool Eindhoven, 1973."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"A. Scedrov. Normalization revisited. In J.W. Gray and A. Scedrov, editors, Proceedings of the AMS research conference, pages 357\u2013369. American Mathematical Society, 1987.","DOI":"10.1090\/conm\/092\/1003209"},{"key":"12_CR19","unstructured":"D.T. van Daalen. The language theory of Automath. PhD thesis, Technische hogeschool Eindhoven, 1980."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037105.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,2]],"date-time":"2024-02-02T14:06:58Z","timestamp":1706882818000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0037105","relation":{},"subject":[]}}