Refined program extraction from classical proofs: Some case studies

MaRDI QIDQ2752052zbMATH OpenFDO

Authors Helmut Schwichtenberg

Publication date 21 October 2001

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Recommendations

• Refined program extraction from classical proofs
• scientific article; zbMATH DE number 895269
• Getting results from programs extracted from classical proofs
• Programs from proofs using classical dependent choice
• Practical program extraction from classical proofs

Cited in

(12)

• Studies of a theory of specifications with built-in program extraction
• Light Dialectica program extraction from a classical Fibonacci proof
• Getting results from programs extracted from classical proofs
• Program extraction from large proof developments
• Programs from proofs using classical dependent choice
• Practical program extraction from classical proofs
• scientific article; zbMATH DE number 2247255 (Why is no real title available?)
• Program extraction from classical proofs
• Refined program extraction from classical proofs
• Extraction of a program from deduction and its regularity. I
• A large-scale experiment in executing extracted programs
• Refinement of classical proofs for program extraction

This page was built for publication: Refined program extraction from classical proofs: Some case studies

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