scientific article; zbMATH DE number 749923

MaRDI QIDQ4764104zbMATH OpenFDO

Authors John N. Crossley, John Shepherdson

Publication date 18 September 1995

zbMATH Keywords

Curry-Howard termsfirst-order predicate calculusgeneral framework for extracting programs from proofsHarrop formula axiomatizationHeyting arithmeticnatural deductionrealizersverifiers

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• Proofs and programs: A naïve approach to program extraction
• Practical program extraction from classical proofs
• scientific article; zbMATH DE number 2003148
• scientific article; zbMATH DE number 2063221

Cited in

(15)

• Extraction and verification of programs by analysis of formal proofs
• Extracting information from intermediate semiconstructive HA-systems -- extended abstract
• Practical program extraction from classical proofs
• Extended Curry-Howard terms for second-order logic
• scientific article; zbMATH DE number 1342285 (Why is no real title available?)
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• Extracting Algorithms from Intuitionistic Proofs
• scientific article; zbMATH DE number 1973215 (Why is no real title available?)
• scientific article; zbMATH DE number 2003148 (Why is no real title available?)
• scientific article; zbMATH DE number 2063221 (Why is no real title available?)
• scientific article; zbMATH DE number 1765700 (Why is no real title available?)
• First order marked types
• Program extraction from classical proofs
• Abbreviation templates
• Proofs and programs: A naïve approach to program extraction

This page was built for publication:

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