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. Momigliano
Primo
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.
Higher order abstract syntax ; Co-induction ; Similarity in the lambda calculus ; Howe’s method ; Abella ; Predicate quantification
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Book Part (author)
File in questo prodotto:
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

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/212809
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? ND
social impact