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

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) 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

(24)

• A verified proof checker for higher-order logic
• Information-flow control on ARM and POWER multicore processors
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A linear first-order functional intermediate language for verified compilers
• Verified characteristic formulae for CakeML
• The verified CakeML compiler backend
• Trace-relating compiler correctness and secure compilation
• A Fast Verified Liveness Analysis in SSA Form
• Automatically Introducing Tail Recursion in CakeML
• A verified compiler for an impure functional language
• CakeML
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML
• Icing: supporting fast-math style optimizations in a verified compiler
• Fully Abstract and Robust Compilation
• Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs
• Verifying software emulation of an unsupported hardware instruction
• Candle: a verified implementation of HOL Light (extended version)
• Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs
• Touring the MetaCoq project
• Fast, verified computation for HOL ITPs
• Certified MaxSAT preprocessing
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs

Describes a project that uses

Uses Software

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

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)