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

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

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)

• Mechanical proofs about computer programs
• Proving and programming
• Non-obfuscated unprovable programs \& many resultant subtleties
• Program verification. Fundamental issues in computer science
• Correctness, explanation and intention
• Checking proofs
• 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)