Sciweavers

PPDP
2007
Springer

Formalizing and verifying semantic type soundness of a simple compiler

13 years 9 months ago
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
Nick Benton, Uri Zarfaty
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where PPDP
Authors Nick Benton, Uri Zarfaty
Comments (0)