Mechanizing type environments in weak HOAS
Autor: | Ivan Scagnetto, Alberto Ciaffaglione |
---|---|
Rok vydání: | 2015 |
Předmět: |
Type theory
Logical frameworks HOAS POPLmark Challenge Type theory POPLmark Challenge General Computer Science business.industry Computer science Programming language Object language System F Proof assistant Representation (systemics) computer.software_genre Theoretical Computer Science HOAS TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Metatheory Logical frameworks Artificial intelligence POPLmark challenge Equivalence (formal languages) business Equivalence (measure theory) computer |
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 |
Externí odkaz: |