Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs

DOI10.1007/978-3-030-51054-1_7MaRDI QIDQ5048997zbMATH OpenOpenAlexFDO

Authors Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-51054-1_7

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Deductive Approach to Program Synthesis
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Bridging the Gap: Automatic Verified Abstraction of C
• CakeML
• Compositional CompCert
• Comprehending monads
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• Proof-producing synthesis of ML from higher-order logic
• Refinement to Imperative/HOL

Cited in

(1)

• Extracting functional programs from Coq, in Coq

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Proof General
• CakeML
• CompCert
• Fiat
• CertiCoq
• Bedrock

This page was built for publication: Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5048997)