We formally verify in Abella that similarity in the call-by-name lambda calculus is a pre-congruence, using Howe’s method. This turns out to be a very challenging task for HOAS-based systems, as it entails a demanding combination of inductive and coinductive reasoning on open terms, for which no other existing HOAS-based system is equipped for. We also o er a proof using a version of Abella supplemented with predicate quantification; this results in a more structured presentation that is largely independent of the operational semantics as well of the chosen notion of (bi)similarity. While the end result is significantly more succinct and elegant than previous attempts, the exercise highlights some limitations of the two-level approach in general and of Abella in particular.
A supposedly fun thing i may have to do again : a HOAS encoding of Howe's method / A. Momigliano - In: LFMTP '12 : proceedings of the seventh International workshop on Logical frameworks and meta-languages, theory and practice : Copenhagen, Denmark, september 9, 2012New York : Association for computing machinery, 2012. - ISBN 9781450315784. - pp. 33-42 (( Intervento presentato al 7. convegno International workshop on Logical frameworks and meta-languages, theory and practice (LFMTP) tenutosi a Copenhagen nel 2012 [10.1145/2364406.2364411].
A supposedly fun thing i may have to do again : a HOAS encoding of Howe's method
A. MomiglianoPrimo
2012
Abstract
We formally verify in Abella that similarity in the call-by-name lambda calculus is a pre-congruence, using Howe’s method. This turns out to be a very challenging task for HOAS-based systems, as it entails a demanding combination of inductive and coinductive reasoning on open terms, for which no other existing HOAS-based system is equipped for. We also o er a proof using a version of Abella supplemented with predicate quantification; this results in a more structured presentation that is largely independent of the operational semantics as well of the chosen notion of (bi)similarity. While the end result is significantly more succinct and elegant than previous attempts, the exercise highlights some limitations of the two-level approach in general and of Abella in particular.File | Dimensione | Formato | |
---|---|---|---|
fun.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
454.39 kB
Formato
Adobe PDF
|
454.39 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.