Code Extraction from Coq to ML-like languages
summary
Pipeline implemented wholly in Coq uses MetaCoq's verified erasure to produce a typed intermediate lambda-box-t representation, runs a certifying preprocessing step (specialization, inlining, unused-argument removal) that emits Coq proofs of semantic preservation, and remaps Coq collection and arithmetic types to primitives so target type checkers succeed. It currently emits working code for CameLIGO and Liquidity plus Elm, and the supplied smart-contract and web-app examples typecheck and execute after extraction.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:16What is code extraction?
- 1:27Extraction in Coq
- 3:03Our extraction pipeline
- 6:14Smart contracts
- 7:29Functional smart contract languages
- 8:30Challenges of new targets
- 12:05Subset types in Coq
- 13:54A counter contract
- 16:08Extracted code in Liquidity
- 16:47Web-programming in Elm
- 18:13Extraction to Elm: Verified web app
- 18:46Verified web app: the model
- 21:05Verified web app: extraction
- 23:03Conclusions
- 24:05Thank you for your attention!
related talks
21mVerified Extraction from Coq to OCaml
45mLogic Meta Programming for Functional Languages
29mMechanized monadic equational reasoning for ML references
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
42mMetaCoq as a tool to prevent future unsoundness in Coq
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
22mA Dependent Language with Type-Safe Program Extraction
23mVellvm: Formalizing the Informal