A certified framework for compiling and executing garbage-collected languages

DOI10.1145/1863543.1863584zbMath1323.68136OpenAlexW2108365678MaRDI QIDQ5176947

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)

Related Items (6)

Verifying a concurrent garbage collector using a rely-guarantee methodology ⋮ The verified CakeML compiler backend ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ GCminor ⋮ Verifying a concurrent garbage collector with a rely-guarantee methodology ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

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

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