Refinement of classical proofs for program extraction

MaRDI QIDQ2876077zbMATH OpenFDO

Authors Diana Ratiu

Publication date 15 August 2014

Full work available at URL http://d-nb.info/1015734464/34

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Proof theory in general (including proof-theoretic semantics) (03F03) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Structure of proofs (03F07)

Recommendations

• Refined program extraction from classical proofs
• Analysis of methods for extraction of programs from non-constructive proofs.
• scientific article; zbMATH DE number 895269
• Programs from proofs using classical dependent choice
• Refined program extraction from classical proofs: Some case studies

Cited in

(11)

• Studies of a theory of specifications with built-in program extraction
• Program extraction in exact real arithmetic
• Completeness, minimal logic and programs extraction
• Analysis of methods for extraction of programs from non-constructive proofs.
• The Peirce translation and the double negation shift
• Decorating proofs
• Programs from proofs using classical dependent choice
• MUS Extraction Using Clausal Proofs
• Program extraction from classical proofs
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• Practical program extraction from classical proofs

This page was built for publication: Refinement of classical proofs for program extraction

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