Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions

DOI10.1007/978-3-319-94205-6_42zbMath1468.68060OpenAlexW2810040629MaRDI QIDQ1799129

Magnus O. Myreen, Ramana Kumar, Oskar Abrahamsson, Michael Norrish, Yong Kiam Tan, Son Lam Ho

Publication date: 18 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94205-6_42

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 (4)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ A verified proof checker for higher-order logic

Uses Software

• Coq
• Isabelle/HOL
• HOL
• CakeML
• CertiCoq
• OEuf

This page was built for publication: Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions