The verified CakeML compiler backend

DOI10.1017/S0956796818000229MaRDI QIDQ4972072zbMATH OpenOpenAlexWikidataFDO

Authors Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, A. C. J. Fox, Scott Owens, Michael Norrish

Publication date 22 November 2019

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796818000229

Mathematics Subject Classification ID

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

Recommendations

• CakeML
• A verified compiler from Isabelle/HOL to CakeML
• A formally verified compiler back-end
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML

Cites work

• A Brief Overview of HOL4
• A certified framework for compiling and executing garbage-collected languages
• A formally verified compiler back-end
• A verified compiler for an impure functional language
• A verified generational garbage collector for CakeML
• A verified runtime for a verified theorem prover
• Automatically Introducing Tail Recursion in CakeML
• CakeML
• Certified complexity (CerCo)
• Certifying and Reasoning on Cost Annotations of Functional Programs
• CompCertTSO
• Compositional CompCert
• Formal verification of coalescing graph-coloring register allocation
• Lightweight verification of separate compilation
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• Proof-producing translation of higher-order logic into pure and stateful ML
• Refinement through restraint: bringing down the cost of verification
• The verified CakeML compiler backend
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• Verified characteristic formulae for CakeML

Cited in

(17)

• Verified characteristic formulae for CakeML
• Icing: supporting fast-math style optimizations in a verified compiler
• A verified generational garbage collector for CakeML
• CakeML
• A verified proof checker for higher-order logic
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Information-flow control on ARM and POWER multicore processors
• The verified CakeML compiler backend
• A verified compiler for an impure functional language
• A verified generational garbage collector for CakeML
• Fully Abstract and Robust Compilation
• A Fast Verified Liveness Analysis in SSA Form
• Trace-relating compiler correctness and secure compilation
• A linear first-order functional intermediate language for verified compilers
• Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs
• Automatically Introducing Tail Recursion in CakeML
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Describes a project that uses

Uses Software

• GCminor
• Pilsner
• MLton
• Poly/ML
• CompCert
• CakeML
• CompCertTSO
• HOL
• gmp
• Coq

This page was built for publication: The verified CakeML compiler backend

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