From proposition to program. Embedding the refinement calculus in Coq

DOI10.1007/978-3-319-29604-3_3MaRDI QIDQ2798255zbMATH OpenOpenAlexFDO

Authors Wouter Swierstra, Joao Alpuim

Publication date 4 April 2016

Published in Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-29604-3_3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Intuitionistic Refinement Calculus
• scientific article; zbMATH DE number 1863389
• Refinement of Higher-Order Logic Programs
• scientific article; zbMATH DE number 177257
• Program Development in Computational Logic

Cites work

• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• scientific article; zbMATH DE number 1104377 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A Hoare Logic for the State Monad
• A program construction and verification tool for separation logic
• An axiomatic basis for computer programming
• Combinator Parsing: A Short Tutorial
• Effective interactive proofs for higher-order imperative programs
• Indexed containers
• Intuitionistic Refinement Calculus
• Programming interfaces and basic topology
• Refinement concepts formalised in higher order logic
• Ynot: dependent types for imperative programs

Cited in

(8)

• scientific article; zbMATH DE number 1670739 (Why is no real title available?)
• Program calculation in Coq
• Proof reflection in Coq
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Intuitionistic Refinement Calculus
• Foundations of dependent interoperability
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)

Describes a project that uses

Uses Software

• Ynot
• Coq

This page was built for publication: From proposition to program. Embedding the refinement calculus in Coq

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