Proofs verifying programs and programs producing proofs: a conceptual analysis

DOI10.1007/978-88-470-0784-0_5MaRDI QIDQ3654815zbMATH OpenOpenAlexFDO

Authors Dag Prawitz

Publication date 11 January 2010

Published in Deduction, Computation, Experiment (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-88-470-0784-0_5

Mathematics Subject Classification ID

Philosophy of mathematics (00A30) Methodology of mathematics (00A35) Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Program verification. Fundamental issues in computer science
• scientific article; zbMATH DE number 4147469
• Proving and programming
• scientific article; zbMATH DE number 3880145
• scientific article; zbMATH DE number 4172362

Cited in

(7)

• Program verification. Fundamental issues in computer science
• Correctness, explanation and intention
• Non-obfuscated unprovable programs \& many resultant subtleties
• Checking proofs
• Mechanical proofs about computer programs
• Proving and programming
• Program analysis is harder than verification: a computability perspective

This page was built for publication: Proofs verifying programs and programs producing proofs: a conceptual analysis

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