Extracting functional programs from Coq, in Coq

DOI10.1017/S0956796822000077OpenAlexW3188083979MaRDI QIDQ5101927

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters

Publication date: 2 September 2022

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2108.02995

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• Coq
• CakeML
• Idris
• CertiCoq
• OEuf
• Template-Coq
• Rust
• MetaCoq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Towards certified meta-programming with typed Template-Coq
• System F in Agda, for fun and profit
• The \textsc{MetaCoq} project
• A verified compiler from Isabelle/HOL to CakeML
• Certified symbolic management of financial multi-party contracts
• Program Extraction from Large Proof Developments
• Pruning simply typed  -terms
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• Syntax and Semantics of Quantitative Type Theory
• Programming Languages and Systems
• Formal certification of a compiler back-end or
• Computer Science Logic
• CakeML
• Erasure and Polymorphism in Pure Type Systems
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• Types for Proofs and Programs
• The Mechanical Evaluation of Expressions
• A Smart Contract for Boardroom Voting with Maximum Voter Privacy

This page was built for publication: Extracting functional programs from Coq, in Coq