Mechanizing type environments in weak HOAS

Autor: Ivan Scagnetto, Alberto Ciaffaglione
Rok vydání: 2015
Předmět:
Zdroj: Theoretical Computer Science. 606:57-78
ISSN: 0304-3975
DOI: 10.1016/j.tcs.2015.07.019
Popis: We provide a paradigmatic case study, about the formalization of System F < : 's type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F < : 's metatheory, on the other hand we address the equivalence of the two approaches internally to Coq.
Databáze: OpenAIRE