scientific article; zbMATH DE number 785043

zbMATH Open0856.03010MaRDI QIDQ4842532FDOQ4842532

Authors: Ulrich Berger, Helmut Schwichtenberg 

Publication date: 26 September 1995

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 140006
• Extraction and verification of programs by analysis of formal proofs
• Program development in constructive type theory
• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 1552509

zbMATH Keywords

natural deductionrecursioninductionexistential quantifierproof systemextracted program of a derivationfragment of minimal logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic programming (68N17) Mechanization of proofs and logical operations (03B35)

Cited In (8)

• Title not available (Why is that?)
• Completeness, minimal logic and programs extraction
• Title not available (Why is that?)
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Towards the computational complexity of \(\mathcal{PR}^ \omega\)-terms
• The greatest common divisor: A case study for program extraction from classical proofs
• Title not available (Why is that?)
• A logic program for transforming sequent proofs to natural deduction proofs

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 Q4842532)