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:
| File | Dimensione | Formato | |
|---|---|---|---|
|
1-s2.0-S1571066104003238-main.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Non pubblico
Dimensione
201.45 kB
Formato
Adobe PDF
|
201.45 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
