A New Extraction for Coq
- 15 April 2003
- book chapter
- Published by Springer Nature
- p. 200-219
- https://doi.org/10.1007/3-540-39185-1_12
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- A Constructive Formalization of the Fundamental Theorem of CalculusPublished by Springer Nature ,2003
- A Constructive Algebraic Hierarchy in CoqJournal of Symbolic Computation, 2002
- A compiled implementation of strong reductionPublished by Association for Computing Machinery (ACM) ,2002
- Studies of a Theory of Specifications with Built-in Program ExtractionJournal of Automated Reasoning, 2001
- Pruning simply typed -termsJournal of Logic and Computation, 1996
- Synthesis of ML programs in the system CoqJournal of Symbolic Computation, 1993
- Extracting ω's programs from proofs in the calculus of constructionsPublished by Association for Computing Machinery (ACM) ,1989