Proofs-as-imperative-programs: application to synthesis of contracts

DOI10.1007/B94823MaRDI QIDQ5902410zbMATH OpenOpenAlexFDO

Authors Iman Poernomo

Publication date 5 January 2010

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

Full work available at URL https://doi.org/10.1007/b94823

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Adapting Proofs-as-Programs
• scientific article; zbMATH DE number 1420787
• Synthesis of Data Views for Communicating Processes
• scientific article; zbMATH DE number 2063228
• Proofs and programs: A naïve approach to program extraction

Cited in

(5)

• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• scientific article; zbMATH DE number 2063228 (Why is no real title available?)
• Abstract contract synthesis and verification in the symbolic \(\mathbb{K}\) framework
• Adapting Proofs-as-Programs
• Contract lenses: Reasoning about bidirectional programs via calculation

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Proofs-as-imperative-programs: application to synthesis of contracts

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