Name
Abstract | ||
|---|---|---|
We develop metatheory of the Lambda calculus in Constructive Type Theory, using a first-order presentation with one sort of names for both free and bound variables and without identifying terms up to α-conversion. Concerning β-reduction, we prove the Church–Rosser theorem and the Subject Reduction theorem for the system of assignment of simple types. It is thereby shown that this concrete approach allows for gentle full formalisation, thanks to the use of an appropriate notion of substitution due to A. Stoughton. The whole development has been machine-checked using the system Agda. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1016/j.tcs.2016.08.025 | Theoretical Computer Science |
Keywords | Field | DocType |
Formal metatheory,Lambda calculus,Type Theory | Deductive lambda calculus,Discrete mathematics,Hindley–Milner type system,Typed lambda calculus,Simply typed lambda calculus,System F,Church encoding,Pure type system,Church–Rosser theorem,Mathematics | Journal |
Volume | ISSN | Citations |
685 | 0304-3975 | 1 |
PageRank | References | Authors |
0.48 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ernesto Copello | 1 | 3 | 2.05 |
| Nora Szasz | 2 | 52 | 8.48 |
| Álvaro Tasistro | 3 | 21 | 2.99 |