Sciweavers

Share
ICFP
2010
ACM

A certified framework for compiling and executing garbage-collected languages

8 years 10 months ago
A certified framework for compiling and executing garbage-collected languages
We describe the design, implementation, and use of a machinecertified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor, that includes primitives for allocating memory in a garbage-collected heap and for specifying GC roots; (ii) a precise, low-level specification for a Cminor library for garbage collection; and (iii) a proven semantics-preserving translation from GCminor to Cminor plus the GC library. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an exampl...
Andrew McCreight, Tim Chevalier, Andrew P. Tolmach
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where ICFP
Authors Andrew McCreight, Tim Chevalier, Andrew P. Tolmach
Comments (0)
books