A weak HOAS approach to the POPLmark Challenge

Alberto Ciaffaglione
(Dipartimento di Matematica e Informatica, Università di Udine, Italia)
Ivan Scagnetto
(Dipartimento di Matematica e Informatica, Università di Udine, Italia)

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.

In Delia Kesner and Petrucio Viana: Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2012), Rio de Janeiro, Brazil, September 29-30, 2012, Electronic Proceedings in Theoretical Computer Science 113, pp. 109–124.
Published: 28th March 2013.

ArXived at: https://dx.doi.org/10.4204/EPTCS.113.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org