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 lowlevel machine. Categories and Subject Descriptors F.3.1 [Logics and meanings of programs]: Specifying and Verifying and Reasoning about Programs—Mechanical verification, Specification techniques; F.3.3 [Logics and meanings of programs]: Studies of Program Constructs— Type structure; D.3.4 [Programming Languages]: Processors— Compilers; D.2.4 [Software Engineering]: Software / Program Verification—Correctness proofs, formal methods General Terms Languages, theory Keywords Compiler verification, type soundness, relational parametricity, separation logic, proof assistants

• Type: Conference
• Year: 2007
• Where: PPDP
• Authors: Nick Benton, Uri Zarfaty
• Keywords: Coq Proof Assistant, PPDP 2007, Proof Assistants, Type Soundness