Formalizing and Verifying Semantic Type Soundness for a Simple Compiler
- Nick Benton ,
- Uri Zarfaty
Proceedings of the Ninth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP '07) |
Published by ACM
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.