Extraction in Coq: An Overview

DOI10.1007/978-3-540-69407-6_39zbMath1142.68498OpenAlexW1522720500MaRDI QIDQ3507450

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)

Related Items (16)

Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof ⋮ Certified Graph View Maintenance with Regular Datalog ⋮ A formally verified compiler back-end ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Schulze voting as evidence carrying computation ⋮ Formally proving size optimality of sorting networks ⋮ Sorting nine inputs requires twenty-five comparisons ⋮ Calculating correct compilers ⋮ Unnamed Item ⋮ Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes ⋮ A Verified LL(1) Parser Generator ⋮ A verified framework for higher-order uncurrying optimizations ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem

Uses Software

• Coq

Cites Work

• Unnamed Item
• Program extraction from normalization proofs
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Program-ing finger trees in C <scp>oq</scp>
• Programming Languages and Systems
• Formal certification of a compiler back-end or

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