 | Adam Koprowski | | personal homepage |
| |
| A Formalization of the Simply Typed Lambda Calculus in Coq |  |
Abstract:
In this paper we present a formalization of the simply typed lambda calculus with constants and with typing `a la Church.
It has been accomplished using the theorem prover Coq. The formalization includes, among other results, definitions of
typed terms over arbitrary many-sorted signature, a substitution operating on typing judgements, an equivalence relation
generalizing the concept of alpha-convertibility to free variables and a proof of strong normalization of beta-reduction.
The formalization has been used in a bigger project of certification of the higher-order recursive path ordering where
well-foundedness of the union of the higher-order recursive path ordering and beta-reduction was the main result.
A Formalization of the Simply Typed Lambda Calculus in Coq Draft |
|
|
|
|
|
|
|
