Compiling Functional Types to Relational Specifications for Low Level Imperative Code

Nick Benton and Nicolas Tabareau

The ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2009)
Savannah, Georgia, USA, Saturday, 24 January, 2009

---

Abstract

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and separation, over stores and values in the low-level machine.

---

START Conference Manager (V2.56.8 - Rev. 399)