We develop metatheory of the Lambda calculus in Constructive Type Theory, using the presentation of the former with one sort of names for both free and bound variables and without identifying terms up to α-conversion. We prove three substitution lemmas: for α-conversion, parallel β-reduction, and for the system of simple type assignment. This work prove the main results of the metatheory; subject reduction of the Type System, and Church-Rosser confluence theorem. This results are possible by the use of an appropriate notion of substitution, due to A. Stoughton. The whole development has been machine-checked using the system Agda. The whole source code is web browsable here.
- Formal metatheory of the Lambda calculus using Stoughton's substitution. Theor. Comput. Sci. 685: 65-82 (2017)
- Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus.. Electr. Notes Theor. Comput. Sci. 312: 215-230 (2015)
- Álvaro Tasistro (Universidad ORT Uruguay)
- Nora Szasz (Universidad ORT Uruguay)
- Ernesto Copello (Universidad ORT Uruguay)
Agda compiler version 2.4.2.5 and standard library version 0.11.