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
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.
Conference Manager (V2.56.8 - Rev. 399)