formalizing and verifying semantic type soundness of a simple compiler
We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and a form of separation structure, over stores and code pointers in the low-level machine.
type soundness proof assistants relational para-metricity separation logic compiler verification