Adapting Proofs-as-Programs

DOI10.1007/0-387-28183-5MaRDI QIDQ5693641zbMATH OpenOpenAlexFDO

Authors Iman Poernomo, John N. Crossley, Martin Wirsing

Publication date 28 September 2005

Published in Monographs in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/0-387-28183-5

zbMATH Keywords

Curry-Howard isomorphismHoare logicintuitionistic logicsynthesis of programs

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proofs-as-imperative-programs: application to synthesis of contracts
• scientific article; zbMATH DE number 2063228
• Synthesis of Data Views for Communicating Processes
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• scientific article; zbMATH DE number 1973215

Cited in

(11)

• Programming in Ωmega
• scientific article; zbMATH DE number 1973215 (Why is no real title available?)
• scientific article; zbMATH DE number 2063228 (Why is no real title available?)
• … and so on: Schütte on Naming Ordinals
• A homage to Martin Wirsing
• Ode to the PST
• Synthesis of functional programs with help of first-order intuitionistic logic
• Synthesis of Data Views for Communicating Processes
• Proofs-as-imperative-programs: application to synthesis of contracts
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

This page was built for publication: Adapting Proofs-as-Programs

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