Proof-producing synthesis of CakeML from monadic HOL functions

DOI10.1007/s10817-020-09559-8zbMath1468.68056OpenAlexW3033813981MaRDI QIDQ2208292

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

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09559-8

zbMATH Keywords

higher-order logicprogram synthesisMLinteractive theorem proving

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)

Uses Software

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

Cites Work

• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Towards certified meta-programming with typed Template-Coq
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• A verified compiler from Isabelle/HOL to CakeML
• Proof-producing translation of higher-order logic into pure and stateful ML
• Refinement to Imperative/HOL
• Verified Characteristic Formulae for CakeML
• Imperative Functional Programming with Isabelle/HOL
• Formal Verification of Coalescing Graph-Coloring Register Allocation
• CakeML

This page was built for publication: Proof-producing synthesis of CakeML from monadic HOL functions