Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
435779 | Theoretical Computer Science | 2015 | 22 Pages |
Abstract
We provide a paradigmatic case study, about the formalization of System F<: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<:F<:'s metatheory, on the other hand we address the equivalence of the two approaches internally to Coq.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Alberto Ciaffaglione, Ivan Scagnetto,