Abstract: We illustrate Nested Abstract Syntax as a high-level alternative representation of languages with binding constructs, based on nested datatypes. Our running example is a partial solution in the Coq proof assistant to the POPLmark Challenge. The resulting formalization is very compact and does not require any extra library or special logical apparatus. Along the way, we propose an original, high-level perspective on environments.
Nested Abstract Syntax in Coq / Maggesi, Marco; Hirschowitz, André. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - STAMPA. - 49:(2012), pp. 1-18. [10.1007/s10817-010-9207-9]
Nested Abstract Syntax in Coq
MAGGESI, MARCO;
2012
Abstract
Abstract: We illustrate Nested Abstract Syntax as a high-level alternative representation of languages with binding constructs, based on nested datatypes. Our running example is a partial solution in the Coq proof assistant to the POPLmark Challenge. The resulting formalization is very compact and does not require any extra library or special logical apparatus. Along the way, we propose an original, high-level perspective on environments.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
nasc.pdf
Accesso chiuso
Tipologia:
Versione finale referata (Postprint, Accepted manuscript)
Licenza:
Tutti i diritti riservati
Dimensione
434.25 kB
Formato
Adobe PDF
|
434.25 kB | Adobe PDF | Richiedi una copia |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
