Programs, proofs and parametrized specifications

DOI10.1007/3-540-45645-7_14MaRDI QIDQ4471724zbMATH OpenFDO

Authors Iman Poernomo, John N. Crossley, Martin Wirsing

Publication date 30 July 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2267/22670280.htm, https://figshare.com/articles/report/Programs_Proofs_and_Parametrized_Specifications/20707768

zbMATH Keywords

CASLCurry-Howard isomorphismParametrized specificationsSML

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Extraction of structured programs from specification proofs
• Studies of a theory of specifications with built-in program extraction
• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 4147469
• Program extraction in simply-typed higher order logic

Cited in

(15)

• Theories for mechanical proofs of imperative programs
• \(QPC_ 2\): A constructive calculus with parameterized specifications
• Algorithms and proofs inheritance in the FOC language
• Extraction of structured programs from specification proofs
• Specification of parameterized programs -- persistency revisited
• Mechanized semantics
• scientific article; zbMATH DE number 48697 (Why is no real title available?)
• Axiomatisations, proofs, and formal specifications of algorithms: Commented case studies in the coq proof assistant
• scientific article; zbMATH DE number 2172806 (Why is no real title available?)
• Holistic Specifications for Robust Programs
• Proofs in parameterized specifications
• scientific article; zbMATH DE number 6403889 (Why is no real title available?)
• Reasoning About Incompletely Defined Programs
• Studies of a theory of specifications with built-in program extraction
• Proof methods of declarative properties of definite programs

This page was built for publication: Programs, proofs and parametrized specifications

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