Mechanizing type environments in weak HOAS
In: Theoretical Computer Science, Jg. 606 (2015-11-01), S. 57-78
Online
unknown
Zugriff:
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.
Titel: |
Mechanizing type environments in weak HOAS
|
---|---|
Autor/in / Beteiligte Person: | Scagnetto, Ivan ; Ciaffaglione, Alberto |
Link: | |
Zeitschrift: | Theoretical Computer Science, Jg. 606 (2015-11-01), S. 57-78 |
Veröffentlichung: | Elsevier BV, 2015 |
Medientyp: | unknown |
ISSN: | 0304-3975 (print) |
DOI: | 10.1016/j.tcs.2015.07.019 |
Schlagwort: |
|
Sonstiges: |
|