A verified compiler from Isabelle/HOL to CakeML

DOI10.1007/978-3-319-89884-1_35zbMath1418.68045OpenAlexW2797934247MaRDI QIDQ2324018

Tobias Nipkow, Lars Hupel

Publication date: 13 September 2019

Full work available at URL: https://doi.org/10.1007/978-3-319-89884-1_35

zbMATH Keywords

Isabellecompilerhigher-order term rewritingCakeML

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Related Items (max. 100)

Introduction to ``Milestones in interactive theorem proving ⋮ Unnamed Item ⋮ Extracting functional programs from Coq, in Coq ⋮ Unnamed Item ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ Amortized complexity verified ⋮ From LCF to Isabelle/HOL ⋮ Efficient verified (UN)SAT certificate checking ⋮ Trustworthy Graph Algorithms (Invited Talk)

Uses Software

• ACL2
• Coq
• Isabelle
• Isabelle/HOL
• HOL
• CakeML
• Pilsner
• Archive Formal Proofs
• Haskell Show Class
• CakeML_Codegen
• Nominal2

This page was built for publication: A verified compiler from Isabelle/HOL to CakeML