Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language of pure System F<: within Coq, a proof assistant based on the Calculus of Inductive Constructions. Our encoding allows us to accomplish the proof of the transitivity property of algorithmic subtyping, which is in fact the first of the three tasks stated by the POPLmark Challenge, a set of problems that capture the most critical issues in formalizing programming language metatheory.
A weak HOAS approach to the POPLmark Challenge
CIAFFAGLIONE, Alberto;SCAGNETTO, Ivan
2013-01-01
Abstract
Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language of pure System F<: within Coq, a proof assistant based on the Calculus of Inductive Constructions. Our encoding allows us to accomplish the proof of the transitivity property of algorithmic subtyping, which is in fact the first of the three tasks stated by the POPLmark Challenge, a set of problems that capture the most critical issues in formalizing programming language metatheory.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
arXiv.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
206.02 kB
Formato
Adobe PDF
|
206.02 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.