From Proposition to Program

DOI10.1007/978-3-319-29604-3_3zbMath1475.68458OpenAlexW2403707805MaRDI QIDQ2798255

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

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

Related Items

Foundations of dependent interoperability, Unnamed Item

Uses Software

• Coq
• Ynot

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Refinement concepts formalised in higher order logic
• Programming interfaces and basic topology
• Effective interactive proofs for higher-order imperative programs
• A Program Construction and Verification Tool for Separation Logic
• A Hoare Logic for the State Monad
• Intuitionistic Refinement Calculus
• Ynot
• Combinator Parsing: A Short Tutorial
• Indexed containers
• An axiomatic basis for computer programming