Furio Honsell, Marino Miculan, Ivan Scagnetto

The Theory of Contexts
for First Order and Higher Order Abstract Syntax


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.


The article is available as a PDF file.
The Coq code of the first case study is available.