The verified CakeML compiler backend
DOI10.1017/S0956796818000229zbMATH Open1493.68091OpenAlexW2912784218WikidataQ122142271 ScholiaQ122142271MaRDI QIDQ4972072FDOQ4972072
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
Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- A Brief Overview of HOL4
- Compositional CompCert
- CompCertTSO
- A certified framework for compiling and executing garbage-collected languages
- Proof-producing translation of higher-order logic into pure and stateful ML
- A Verified Runtime for a Verified Theorem Prover
- CakeML
- A formally verified compiler back-end
- Verified Characteristic Formulae for CakeML
- Certifying and Reasoning on Cost Annotations of Functional Programs
- Certified Complexity (CerCo)
- A verified compiler for an impure functional language
- Automatically Introducing Tail Recursion in CakeML
- Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
- Formal Verification of Coalescing Graph-Coloring Register Allocation
- The verified CakeML compiler backend
- Refinement through restraint: bringing down the cost of verification
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- A verified generational garbage collector for CakeML
- Lightweight verification of separate compilation
Cited In (14)
- A verified generational garbage collector for CakeML
- CakeML
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- A verified proof checker for higher-order logic
- Trace-Relating Compiler Correctness and Secure Compilation
- Verified Characteristic Formulae for CakeML
- Information-flow control on ARM and POWER multicore processors
- The verified CakeML compiler backend
- A verified generational garbage collector for CakeML
- Fully Abstract and Robust Compilation
- A Fast Verified Liveness Analysis in SSA Form
- 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
Uses Software
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)
