Extraction in Coq: An Overview

DOI10.1007/978-3-540-69407-6_39MaRDI QIDQ3507450zbMATH OpenOpenAlexFDO

Authors Pierre Letouzey

Publication date 19 June 2008

Published in Logic and Theory of Algorithms (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69407-6_39

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 2003158
• Extracting functional programs from Coq, in Coq
• scientific article; zbMATH DE number 2061716
• Optimized program extraction for induction and coinduction
• Program Extraction in Constructive Analysis
• Program extraction via typed realisability for induction and coinduction
• An operational approach to program extraction in the calculus of constructions
• Subset Coercions in Coq
• Inductive and coinductive components of corecursive functions in Coq

Cites work

• A large-scale experiment in executing extracted programs
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Program extraction from normalization proofs
• Program-ing finger trees in Coq
• Programming Languages and Systems

Cited in

(23)

• Scallina: translating verified programs from Coq to Scala
• The Scallina grammar. Towards a Scala extraction for Coq
• Formally verifying the solution to the Boolean Pythagorean triples problem
• Extracting Purely Functional Contents from Logical Inductive Types
• A formally verified compiler back-end
• A verified framework for higher-order uncurrying optimizations
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• A certified reduction strategy for homological image processing
• Functional encryption for inner product with full function privacy
• scientific article; zbMATH DE number 2061716 (Why is no real title available?)
• scientific article; zbMATH DE number 7471663 (Why is no real title available?)
• Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes
• Computer Certified Efficient Exact Reals in Coq
• A Verified LL(1) Parser Generator
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• Extracting functional programs from Coq, in Coq
• Certified Graph View Maintenance with Regular Datalog
• Schulze voting as evidence carrying computation
• Sorting nine inputs requires twenty-five comparisons
• Extraction in the Lambek-Grishin Calculus
• Formally proving size optimality of sorting networks
• Animating the formalised semantics of a Java-like language
• Calculating correct compilers

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Extraction in Coq: An Overview

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