A verified generational garbage collector for CakeML

DOI10.1007/978-3-319-66107-0_28zbMath1468.68065OpenAlexW2747308484MaRDI QIDQ5915786

Adam Sandberg Ericsson, Johannes Åman Pohjola, Magnus O. Myreen

Publication date: 4 January 2018

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://research.chalmers.se/en/publication/252200

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

A verified generational garbage collector for CakeML ⋮ The verified CakeML compiler backend ⋮ Verifying a concurrent garbage collector with a rely-guarantee methodology

Uses Software

• Isabelle/HOL
• HOL
• CakeML
• Milawa
• CertiCoq

Cites Work

• Unnamed Item
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• A mechanically verified incremental garbage collector
• A Verified Runtime for a Verified Theorem Prover
• Formal Derivation of Concurrent Garbage Collectors
• On-the-fly garbage collection
• The verified CakeML compiler backend
• Automated verification of practical garbage collectors

This page was built for publication: A verified generational garbage collector for CakeML