{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:44Z","timestamp":1751660504310},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540580850"},{"type":"electronic","value":"9783540484400"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58085-9_82","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:11:20Z","timestamp":1330269080000},"page":"313-332","source":"Crossref","is-referenced-by-count":19,"title":["Closure under alpha-conversion"],"prefix":"10.1007","author":[{"given":"Randy","family":"Pollack","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"4","key":"14_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. Levy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, October 1991.","journal-title":"Journal of Functional Programming"},{"doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, March 1993.","key":"14_CR2","DOI":"10.1007\/BFb0037095"},{"issue":"2","key":"14_CR3","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"Henk Barendregt. Introduction to generalised type systems. J. Functional Programming, 1(2):125\u2013154, April 1991.","journal-title":"J. Functional Programming"},{"doi-asserted-by":"crossref","unstructured":"Henk Barendregt. Lambda calculi with types. In Gabbai Abramsky and. Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.","key":"14_CR4","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"14_CR5","volume-title":"PhD thesis","author":"S. Berardi","year":"1990","unstructured":"Stefano Berardi. Type Dependence and Constructive Mathematics. PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990."},{"doi-asserted-by":"crossref","unstructured":"Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. D. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.","key":"14_CR6","DOI":"10.1017\/CBO9780511569807.011"},{"doi-asserted-by":"crossref","unstructured":"Nicolas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the churchrosser theorem. Indag. Math., 34(5), 1972.","key":"14_CR7","DOI":"10.1016\/1385-7258(72)90034-0"},{"unstructured":"Nicolas G. de Bruijn. Generalizing automath by means of a lambda-typed lambda calculus. In Proceedings of the Maryland 1984\u20131985 Special Year in Mathematical Logic and Theoretical Computer Science, 1985.","key":"14_CR8"},{"unstructured":"Dowek, Felty, Herbelin, Huet, Murthy, Parent, Paulin-Mohring, and Werner. The Coq proof assistant user's guide, version 5.8. Technical report, INRIA-Rocquencourt, February 1993.","key":"14_CR9"},{"issue":"2","key":"14_CR10","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Herman Geuvers and Mark-Jan Nederhof. A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155\u2013189, April 1991.","journal-title":"Journal of Functional Programming"},{"unstructured":"Andrew Gordon. A mechanism of name-carrying syntax up to alphaconversion. In Proceedings of the 1993 HOL User's Meeting, Vancouver. Springer-Verlag, 1993. LNCS.","key":"14_CR11"},{"issue":"1","key":"14_CR12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1992","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, 1992. Preliminary version in LICS'87.","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"G\u00e9rard Huet. The constructive engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing, 1989. Commemorative Volume for Gift Siromoney.","key":"14_CR13","DOI":"10.1142\/0867"},{"unstructured":"G. Huet. Residual theory in \u03bb-calculus: A complete Gallina development. 1993.","key":"14_CR14"},{"key":"14_CR15","volume-title":"Technical Report ECS-LFCS-92-211","author":"Z. Luo","year":"1992","unstructured":"Zhaohui Luo and Robert Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, May 1992. Updated version."},{"unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, June 1990.","key":"14_CR16"},{"doi-asserted-by":"crossref","unstructured":"James McKinna and Robert Pollack. Pure type systems formalized. In M.Bezem and J.F.Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, pages 289\u2013305. Springer-Verlag, LNCS 664, March 1993.","key":"14_CR17","DOI":"10.1007\/BFb0037093"},{"unstructured":"Robert Pollack. Implicit syntax. Informal Proceedings of First Workshop on Logical Frameworks, Antibes, May 1990.","key":"14_CR18"},{"unstructured":"R. Pollack. Typechecking in pure type systems. In Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, pages 271\u2013288, June 1992. available by ftp.","key":"14_CR19"},{"unstructured":"Robert Pollack. The Theory of LEGO; A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994. In preparation.","key":"14_CR20"},{"unstructured":"A. Tasistro. Formulation of Martin-L\u00f6f 's theory of types with explicit substitutions. Master's thesis, Chalmers Tekniska H\u00f6gskola and G\u00f6teborgs Universitet, May 1993.","key":"14_CR21"},{"issue":"1","key":"14_CR22","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L.S. Benthem Jutting van","year":"1993","unstructured":"L.S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 105(1):30\u201341, July 1993.","journal-title":"Information and Computation"},{"unstructured":"L.S. van Benthem Jutting, James McKinna, and Robert Pollack. Typechecking in pure type systems. In Henk Barendregt and Tobias Nipkow, editors, Formal Proceedings of the Nijmegen Workshop on Types for Proofs and Programs, May '93. Springer-Verlag, LNCS, 1994. This volume.","key":"14_CR23"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58085-9_82.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T15:44:10Z","timestamp":1713627850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58085-9_82"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580850","9783540484400"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-58085-9_82","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}