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

DOI10.1007/978-3-030-51054-1_7OpenAlexW3037570434MaRDI QIDQ5048997

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

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)

Related Items (1)

Extracting functional programs from Coq, in Coq

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• Compositional CompCert
• Fiat
• Bridging the Gap: Automatic Verified Abstraction of C
• Refinement to Imperative/HOL
• A Deductive Approach to Program Synthesis
• Comprehending monads
• Proof-producing synthesis of ML from higher-order logic
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Formal certification of a compiler back-end or
• CakeML

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