{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,3]],"date-time":"2025-10-03T17:49:23Z","timestamp":1759513763999,"version":"3.40.5"},"reference-count":20,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T00:00:00Z","timestamp":1637884800000},"content-version":"unspecified","delay-in-days":270,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,3]]},"abstract":"<jats:title>Abstarct<\/jats:title><jats:p>We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with <jats:italic>\u03b1<\/jats:italic>-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction\/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church\u2013Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.<\/jats:p>","DOI":"10.1017\/s0960129521000335","type":"journal-article","created":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T03:58:34Z","timestamp":1637899114000},"page":"341-360","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention"],"prefix":"10.1017","volume":"31","author":[{"given":"Ernesto","family":"Copello","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8177-8695","authenticated-orcid":false,"given":"Nora","family":"Szasz","sequence":"additional","affiliation":[]},{"given":"\u00c1lvaro","family":"Tasistro","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,11,26]]},"reference":[{"key":"S0960129521000335_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-6604-5"},{"key":"S0960129521000335_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.018"},{"key":"S0960129521000335_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.06.008"},{"key":"S0960129521000335_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"S0960129521000335_ref16","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"S0960129521000335_ref18","doi-asserted-by":"crossref","unstructured":"Urban, C. , Berghofer, S. and Norrish, M. (2007). Barendregt\u2019s variable convention in rule inductions, 35\u201350.","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"S0960129521000335_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.006"},{"key":"S0960129521000335_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.028"},{"key":"S0960129521000335_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"S0960129521000335_ref8","unstructured":"Copello, E. (2017). On the Formalisation of the Metatheory of the Lambda Calculus and Languages with Binders. Phd thesis, Universidad ORT Uruguay."},{"key":"S0960129521000335_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-002-0156-9"},{"key":"S0960129521000335_ref4","unstructured":"Barendregt, H. (1984). The \u03bb-calculus Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, revised edition, vol. 103, North Holland."},{"key":"S0960129521000335_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_41"},{"key":"S0960129521000335_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.009"},{"key":"S0960129521000335_ref11","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.2"},{"key":"S0960129521000335_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S0960129521000335_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"year":"2005","author":"Urban","key":"S0960129521000335_ref19"},{"key":"S0960129521000335_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.08.025"},{"key":"S0960129521000335_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00023-3"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,20]],"date-time":"2021-12-20T13:14:28Z","timestamp":1640006068000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000335\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["S0960129521000335"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000335","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,3]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}