Practical program extraction from classical proofs

MaRDI QIDQ2852367zbMATH OpenFDO

Authors Yevgeniy Makarov

Publication date 8 October 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066106002088

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Program extraction from classical proofs
• Refined program extraction from classical proofs
• Refinement of classical proofs for program extraction
• Refined program extraction from classical proofs: Some case studies
• Getting results from programs extracted from classical proofs
• Proofs and programs: A naïve approach to program extraction
• Classical Program Extraction in the Calculus of Constructions
• Program extraction from large proof developments
• scientific article; zbMATH DE number 749923
• scientific article; zbMATH DE number 1617311

Cited in

(21)

• Programming and Proving with Classical Types
• Refined program extraction from classical proofs: Some case studies
• Extracting Algorithms from Intuitionistic Proofs
• Program extraction in exact real arithmetic
• Existential witness extraction in classical realizability and via a negative translation
• Classical extraction in continuation models
• Classical Program Extraction in the Calculus of Constructions
• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
• Classical proofs as programs: how, what and why
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Extraction of a program from deduction and its regularity. I
• scientific article; zbMATH DE number 517083 (Why is no real title available?)
• MUS Extraction Using Clausal Proofs
• Program extraction from classical proofs
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• Controlling Program Extraction in Light Logics
• Getting results from programs extracted from classical proofs
• Refined program extraction from classical proofs
• Uniform Heyting arithmetic
• Dependent choice, `quote' and the clock

This page was built for publication: Practical program extraction from classical proofs

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