We present two case studies in formal reasoning about untyped λ-calculus in Coq, using both first-order and higher-order abstract syntax. In the first case, we prove the equivalence of three definitions of α-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 Theory of Contexts for First Order and Higher Order Abstract Syntax
HONSELL, Furio;MICULAN, Marino;SCAGNETTO, Ivan
2001-01-01
Abstract
We present two case studies in formal reasoning about untyped λ-calculus in Coq, using both first-order and higher-order abstract syntax. In the first case, we prove the equivalence of three definitions of α-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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
