A certified framework for compiling and executing garbage-collected languages

DOI10.1145/1863543.1863584MaRDI QIDQ5176947zbMATH OpenOpenAlexFDO

Authors Andrew Mccreight, Tim Chevalier, Andrew Tolmach

Publication date 5 March 2015

Published in Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1863543.1863584

zbMATH Keywords

program proofgarbage collectionCoq theorem provercertified compilationHaskell compilation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Recommendations

• Formal Certification of a Resource-Aware Language Implementation
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML
• Certifying compilation and run-time code generation
• scientific article; zbMATH DE number 1701349

Cited in

(8)

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Cogent: uniqueness types and certifying compilation
• GCminor
• A verified runtime for a verified theorem prover
• The verified CakeML compiler backend
• Program logic and equivalence in the presence of garbage collection.
• A verified generational garbage collector for CakeML
• Verifying a concurrent garbage collector using a rely-guarantee methodology

Describes a project that uses

Uses Software

• MLCompCert
• cminor
• CompCert
• GHC
• OCaml
• Haskell
• Coq

This page was built for publication: A certified framework for compiling and executing garbage-collected languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5176947)