We
present two case studies in formal reasoning about untyped lambda-calculus
in Coq, using both first-order and higher-order abstract syntax.
In the first case, we prove the equivalence of three definitions
of alpha-equivalence; in the second, we focus on properties of
substitution. In both cases, we deal with contexts, which are
rendered by means of higher-order terms (functions) in the metalanguage.
These are successfully handled by using the Theory of Contexts. |
Papers
