{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:55Z","timestamp":1781172355192,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615873","type":"print"},{"value":"9783540706410","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105404","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"173-190","source":"Crossref","is-referenced-by-count":38,"title":["Five axioms of alpha-conversion"],"prefix":"10.1007","author":[{"given":"Andrew D.","family":"Gordon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"12_CR1","unstructured":"Barendregt, H. P. (1984). The Lambda Calculus: Its Syntax and Semantics (Revised ed.), Volume 103 of Studies in logic and the foundations of mathematics. North-Holland."},{"key":"12_CR2","unstructured":"Boulton, R., A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel (1992). Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute (Eds.), 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, pp. 129\u2013156. North-Holland."},{"key":"12_CR3","unstructured":"Church, A. (1941). The Calculi of Lambda-Conversion. Princeton University Press."},{"key":"12_CR4","unstructured":"Curry, H. B. and R. Feys (1958). Combinatory Logic, Volume 1. North-Holland."},{"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":"de Bruijn, N. G. (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, 381\u2013392.","journal-title":"Indagationes Mathematicae"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Despeyroux, J. and A. Hirschowitz (1994, July). Higher-order abstract syntax with induction in Coq. In F. Pfenning (Ed.), Fifth International Conference on Logic Programming and Automated Reasoning (LPAR'94), Kiev, Volume 882 of LNAI, pp. 159\u2013173. Springer-Verlag.","DOI":"10.1007\/3-540-58216-9_36"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Gordon, A. D. (1994). A mechanisation of name-carrying syntax up to alpha-conversion. In J. J. Joyce and C.-J. H. Seger (Eds.), Higher Order Logic Theorem Proving and its Applications. Proceedings, 1993, Number 780 in Lecture Notes in Computer Science, pp. 414\u2013426. Springer-Verlag.","DOI":"10.1007\/3-540-57826-9_152"},{"key":"12_CR8","unstructured":"Gordon, M. J. C. and T. F. Melham (Eds.) (1993). Introduction to HOL: A theorem-proving environment for higher-order logic. Cambridge University Press."},{"key":"12_CR9","unstructured":"Hindley, J. R. and J. P. Seldin (1986). Introduction to Combinators and the \u03bb-calculus. Cambridge University Press."},{"key":"12_CR10","unstructured":"Lambek, J. and P. J. Scott (1986). Introduction to higher order categorical logic. Cambridge University Press."},{"key":"12_CR11","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P. J. Landin","year":"1964","unstructured":"Landin, P. J. (1964, January). The mechanical evaluation of expressions. Computer Journal 6, 308\u2013320.","journal-title":"Computer Journal"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Matthews, S. (1995, September). Implementing FS 0 in Isabelle: adding structure at the metalevel. In L. C. Paulson (Ed.), Proceedings of the First Isabelle Users Workshop. Available as Technical Report 379, University of Cambridge Computer Laboratory.","DOI":"10.1007\/3-540-61697-7_24"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"McKinna, J. and R. Pollack (1993). Pure Type Systems formalized. In TLCA\u2019 93 International Conference on Typed Lambda Calculi and Applications, Utrecht, 16\u201318 March 1993, Volume 664 of Lecture Notes in Computer Science, pp. 289\u2013305. Springer-Verlag.","DOI":"10.1007\/BFb0037113"},{"key":"12_CR14","first-page":"50","volume":"1","author":"T. F. Melham","year":"1994","unstructured":"Melham, T. F. (1994). A mechanized theory of the \u03c0-calculus in HOL. Nordic Journal of Computing 1, 50\u201376.","journal-title":"Nordic Journal of Computing"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., J. Parrow, and D. Walker (1992). A calculus of mobile processes, parts I and II. Information and Computation 100, 1\u201340 and 41\u201377.","journal-title":"Information and Computation"},{"key":"12_CR16","volume-title":"Programming in Martin-L\u00f6f's Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., K. Petersson, and J. M. Smith (1990). Programming in Martin-L\u00f6f's Type Theory. Clarendon Press, Oxford."},{"key":"12_CR17","unstructured":"Owens, C. (1995, September). Coding binding and substitution explicitly in Isabelle. In L. C. Paulson (Ed.), Proceedings of the First Isabelle Users Workshop. Available as Technical Report 379, University of Cambridge Computer Laboratory."},{"key":"12_CR18","unstructured":"Paulson, L. C. (1994). Isabelle: A Generic Theorem Prover, Volume 828 of Lecture Notes in Computer Science. Springer-Verlag."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and C. Elliott (1988, June). Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN\u2019 88 Symposium on Language Design and Implementation, pp. 199\u2013208.","DOI":"10.1145\/53990.54010"},{"key":"12_CR20","unstructured":"Pollack, R. (1994). The Theory of LEGO. Ph. D. thesis, University of Edinburgh."},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","volume":"59","author":"A. Stoughton","year":"1988","unstructured":"Stoughton, A. (1988). Substitution revisited. Theoretical Computer Science 59, 317\u2013325.","journal-title":"Theoretical Computer Science"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(93)90240-T","volume":"112","author":"C. L. Talcott","year":"1993","unstructured":"Talcott, C. L. (1993). A theory of binding structures and applications to rewriting. Theoretical Computer Science 112, 99\u2013143.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105404","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T05:44:00Z","timestamp":1560923040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105404"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0105404","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}