We formulate principles of induction and recursion for a variant of lambda calculus with bound names where alpha-conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo alpha-conversion and apply the Barendregt variable convention. We derive them all from the simple structural induction principle and apply them to get some fundamental meta-theoretical results, such as the substitution lemma for alpha-conversion and the result of substitution composition. The whole work is implemented in Agda, and is browsable here.
- Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory. Electr. Notes Theor. Comput. Sci. 323: 109-124 (2016)
- Ana Bove (Chalmers University of Technology)
- Ernesto Copello (Universidad ORT Uruguay)
- Maribel Fernandez (King's College London)
- Nora Szasz (Universidad ORT Uruguay)
- Álvaro Tasistro (Universidad ORT Uruguay)
Agda compiler version 2.5.1 and standard library version 0.12
Machine-checked proof of the Church-Rosser theorem for Lambda-Calculus using the Barendregt Variable Convention in Constructive Type Theory, Electronic Notes in Theoretical Computer Science,2018 in press.