The verified CakeML compiler backend

DOI10.1017/S0956796818000229zbMath1493.68091OpenAlexW2912784218WikidataQ122142271 ScholiaQ122142271MaRDI QIDQ4972072

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

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)

Related Items

Trace-Relating Compiler Correctness and Secure Compilation, A Fast Verified Liveness Analysis in SSA Form, Automatically Introducing Tail Recursion in CakeML, Information-flow control on ARM and POWER multicore processors, Verified Characteristic Formulae for CakeML, Characteristic formulae for liveness properties of non-terminating CakeML programs, \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML, A verified proof checker for higher-order logic, A verified generational garbage collector for CakeML, A verified generational garbage collector for CakeML, The verified CakeML compiler backend

Uses Software

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

Cites Work

• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• A formally verified compiler back-end
• Compositional CompCert
• Lightweight verification of separate compilation
• Proof-producing translation of higher-order logic into pure and stateful ML
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• Refinement through restraint: bringing down the cost of verification
• Verified Characteristic Formulae for CakeML
• A Verified Runtime for a Verified Theorem Prover
• Certifying and Reasoning on Cost Annotations of Functional Programs
• Certified Complexity (CerCo)
• A Brief Overview of HOL4
• Formal Verification of Coalescing Graph-Coloring Register Allocation
• The verified CakeML compiler backend
• Automatically Introducing Tail Recursion in CakeML
• A certified framework for compiling and executing garbage-collected languages
• A verified compiler for an impure functional language
• CompCertTSO
• CakeML
• A verified generational garbage collector for CakeML