Compiling Functional Types to Relational Specifications for Low Level Imperative Code
- Nick Benton ,
- Nicolas Tabareau
Proceedings of the Fourth ACM SIGPLAN Workshop on Types in Language Design and Implementation |
Published by Association for Computing Machinery, Inc.
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.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. The definitive version of this paper can be found at ACM's Digital Library --http://www.acm.org/dl/.