{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:52Z","timestamp":1742617132514,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540565031"},{"type":"electronic","value":"9783540475743"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56503-5_73","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:17:29Z","timestamp":1330255049000},"page":"712-723","source":"Crossref","is-referenced-by-count":0,"title":["Defining \u03bb-typed \u03bb-calculi by axiomatizing the typing relation"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Groote","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"issue":"4","key":"73_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"73_CR2","unstructured":"H.P. Barendregt. The lambda calculus, its syntax and semantics. North-Holland, revised edition, 1984."},{"issue":"2","key":"73_CR3","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":"73_CR4","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":"73_CR5","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":"73_CR6","unstructured":"N.G. de Bruijn. AUT-SL, a single line version of AUTOMATH. Technical Report AUT 20, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1971."},{"key":"73_CR7","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":"73_CR8","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":"73_CR9","series-title":"Lecture Notes in pure and applied Mathematics","first-page":"71","volume-title":"Mathematical Logic and Theoretical Computer Science","author":"N. G. Bruijn de","year":"1987","unstructured":"N.G. de Bruijn. Generalizing automath by means of a lambda-typed lambda-calculus. In Mathematical Logic and Theoretical Computer Science, pages 71\u201392. Lecture Notes in pure and applied Mathematics, 106, Marcel Dekker, New York, 1987."},{"key":"73_CR10","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn. A plea for weaker frameworks. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 40\u201367. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.004"},{"key":"73_CR11","unstructured":"N.G. de Bruijn. Algorithmic definition of \u03bb-typed \u03bb-calculus. In G. Huet and G. Plotkin, editors, Logical Environments. Cambridge University Press, 1992."},{"key":"73_CR12","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":"73_CR13","doi-asserted-by":"crossref","unstructured":"Ph. de Groote. Nederpelt's calculus extended with a notion of context as a logical framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 69\u201386. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.005"},{"key":"73_CR14","doi-asserted-by":"crossref","unstructured":"H. Genvers. The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In Proceedings of the seventh annual IEEE symposium on logic in computer science, pages 453\u2013460, 1992.","DOI":"10.1109\/LICS.1992.185556"},{"issue":"2","key":"73_CR15","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.-J. Nederhof. 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":"73_CR16","unstructured":"R. Harper, F. Honsel, 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":"73_CR17","doi-asserted-by":"crossref","unstructured":"R. Harper and F. Pfenning. A module systems for a programming language based on the If logical framework. Submitted for publication, 1992.","DOI":"10.21236\/ADA256731"},{"key":"73_CR18","doi-asserted-by":"crossref","unstructured":"G. Huet and G. Plotkin, editors. Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807"},{"key":"73_CR19","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In Logic Colloquium '73, pages 73\u2013118. North-Holland, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"73_CR20","unstructured":"R.P. Nederpelt. Strong normalization in a typed lambda calculus with lambda structured types. PhD thesis, Technische hogeschool Eindhoven, 1973."},{"key":"73_CR21","doi-asserted-by":"crossref","unstructured":"R.P. Nederpelt. An approach to theorem proving on the basis of a typed lambdacalculus. In Proceedings of the 5th international conference on automated deduction, pages 182\u2013194. Lecture Notes in Computer Science, 87, Springer Verlag, 1980.","DOI":"10.1007\/3-540-10009-1_15"},{"key":"73_CR22","unstructured":"R.P. Nederpelt. The fine-structure of lambda calculus. Computing Science Notes. Eindhoven University of Technology, 1992."},{"key":"73_CR23","unstructured":"L.C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013386. Academic Press, 1990."},{"key":"73_CR24","unstructured":"D.T. van Daalen. The language theory of Automath. PhD thesis, Technische hogeschool Eindhoven, 1980."}],"container-title":["Lecture Notes in Computer Science","STACS 93"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56503-5_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:50:17Z","timestamp":1742593817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56503-5_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540565031","9783540475743"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-56503-5_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}