{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T16:57:03Z","timestamp":1789923423348,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540578260","type":"print"},{"value":"9783540483465","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_152","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:59Z","timestamp":1330262819000},"page":"413-425","source":"Crossref","is-referenced-by-count":20,"title":["A mechanisation of name-carrying syntax up to alpha-conversion"],"prefix":"10.1007","author":[{"given":"Andrew D.","family":"Gordon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"4","key":"32_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, October 1991.","journal-title":"Journal of Functional Programming"},{"key":"32_CR2","unstructured":"Samson Abramsky. The lazy lambda calculus. In David Turner, editor, Research Topics in Functional Programming, pages 65\u2013116. Addison-Wesley, 1990."},{"key":"32_CR3","first-page":"13","volume-title":"volume 664 of Lecture Notes in Computer Science","author":"T. Altenkirch","year":"1993","unstructured":"Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In TLCA '93 International Conference on Typed Lambda Calculi and Applications, Utrecht, 16\u201318 March 1993, volume 664 of Lecture Notes in Computer Science, pages 13\u201328. Springer-Verlag, 1993."},{"key":"32_CR4","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, revised edition, 1984."},{"key":"32_CR5","first-page":"129","volume-title":"IFIP Transactions A-10","author":"R. Boulton","year":"1992","unstructured":"Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10\/WG 10.2 International Conference, Nijmegen, June 1992, IFIP Transactions A-10, pages 129\u2013156. North-Holland, 1992."},{"issue":"3","key":"32_CR6","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","volume":"36","author":"A. Church","year":"1936","unstructured":"Alonzo Church and J. B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 36(3):472\u2013482, May 1936.","journal-title":"Transactions of the American Mathematical Society"},{"key":"32_CR7","unstructured":"Catarina Coquand. A machine assisted semantical analysis of simply typed lambda calculus. In P. Dybjer, J. Hughes, A. Moran, and B. Nordstr\u00f6m, editors, Proceedings of El Winterm\u00f6te, pages 92\u2013100. Programming Methodology Group, Chalmers University of Technology and University of Gothenburg, June 1993. Available as Report 73."},{"key":"32_CR8","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 notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381\u2013392, 1972.","journal-title":"Indagationes Mathematicae"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Jo\u00eblle Despeyroux and Andr\u00e9 Hirschowitz. Higher-order abstract syntax and induction. Transparencies for a talk at the Types BRA Workshop on Proving Properties of Programming Languages, Sophia-Antipolis, September 1993.","DOI":"10.1007\/3-540-58216-9_36"},{"key":"32_CR10","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theoremproving environment for higher-order logic. Cambridge University Press, 1993."},{"key":"32_CR11","unstructured":"Michael J. C. Gordon. Mechanizing programming logics in higher order logic. Technical Report 145, University of Cambridge Computer Laboratory, September 1988."},{"key":"32_CR12","first-page":"365","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"E. L. Gunter","year":"1992","unstructured":"Elsa L. Gunter. Why we can't have SML style datatype declarations in HOL. In L. Claesen and M. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, pages 365\u2013372, Leuven, 1992. IMEC."},{"key":"32_CR13","unstructured":"J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and \u03bb-Calculus. Cambridge University Press, 1986."},{"key":"32_CR14","unstructured":"G\u00e9rard Huet. Residual theory in \u03bb-calculus: A complete Gallina development. Preprint, 1992."},{"key":"32_CR15","first-page":"289","volume-title":"volume 664 of Lecture Notes in Computer Science","author":"J. McKinna","year":"1993","unstructured":"James McKinna and Robert Pollack. Pure Type Systems formalized. In TLCA '93 International Conference on Typed Lambda Calculi and Applications, Utrecht, 16\u201318 March 1993, volume 664 of Lecture Notes in Computer Science, pages 289\u2013305. Springer-Verlag, 1993."},{"key":"32_CR16","unstructured":"T. F. Melham. The HOL pred_sets Library. University of Cambridge Computer Laboratory, February 1992."},{"key":"32_CR17","first-page":"350","volume-title":"A package for inductive relation definitions in HOL","author":"T. F. Melham","year":"1991","unstructured":"Thomas F. Melham. A package for inductive relation definitions in HOL. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, pages 350\u2013357. IEEE Computer Society Press, 1991."},{"key":"32_CR18","unstructured":"Thomas F. Melham. A mechanized theory of the \u03c0-calculus in HOL. Technical Report 244, University of Cambridge Computer Laboratory, January 1992."},{"key":"32_CR19","unstructured":"Thomas Frederick Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, University of Cambridge Computer Laboratory, August 1990. Available as Technical Report 201."},{"key":"32_CR20","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, Mass., 1990."},{"key":"32_CR21","unstructured":"Monica Nesi. A formalization of the process algebra CCS in higher order logic. Technical Report 278, University of Cambridge Computer Laboratory, December 1992."},{"key":"32_CR22","unstructured":"Bengt Nordstr\u00f6m. Martin-L\u00f6f's type theory as a programming logic. Report 27, Programming Methodology Group, Chalmers University of Technology and University of Gothenburg, September 1986."},{"key":"32_CR23","unstructured":"Lawrence C. Paulson. ML for the Working Programmer.Cambridge University Press, 1991."},{"key":"32_CR24","unstructured":"Lawrence C. Paulson. The Isabelle reference manual. Internal report, University of Cambridge Computer Laboratory, 1992."},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. A proof of the Church-Rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, Computer Science Dept., Carnegie Mellon University, September 1992.","DOI":"10.21236\/ADA256574"},{"key":"32_CR26","doi-asserted-by":"crossref","unstructured":"Randy Pollack. Closure under alpha-conversion. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, September 1993.","DOI":"10.1007\/3-540-58085-9_82"},{"issue":"3","key":"32_CR27","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1145\/44483.44484","volume":"35","author":"N. Shankar","year":"1988","unstructured":"N. Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 35(3):475\u2013522, July 1988.","journal-title":"Journal of the ACM"},{"key":"32_CR28","doi-asserted-by":"crossref","unstructured":"J. von Wright. Representing higher-order logic proofs in HOL. University of Cambridge Computer Laboratory, July 1993.","DOI":"10.1007\/3-540-58450-1_60"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_152.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:31Z","timestamp":1605647671000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_152","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}