scientific article; zbMATH DE number 2063228

MaRDI QIDQ4460845zbMATH OpenFDO

Authors Iman Poernomo, John N. Crossley

Publication date 29 March 2004

zbMATH Keywords

automated theorem provingconstructive type theoryCurry-Howard isomorphismHoare logicimperative programsprogram specification

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Adapting Proofs-as-Programs
• Synthesis of functional programs with help of first-order intuitionistic logic
• Proofs-as-imperative-programs: application to synthesis of contracts
• Lectures on the Curry-Howard isomorphism
• scientific article; zbMATH DE number 1342285

Cited in

(8)

• Typing in reflective combinatory logic
• Variations on a theme of Curry
• iRho: an imperative rewriting calculus
• scientific article; zbMATH DE number 1342285 (Why is no real title available?)
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Synthesis of functional programs with help of first-order intuitionistic logic
• Adapting Proofs-as-Programs
• Proofs-as-imperative-programs: application to synthesis of contracts

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