A Hoare Logic for the State Monad

DOI10.1007/978-3-642-03359-9_30zbMath1252.68067OpenAlexW101014555MaRDI QIDQ3183544

Wouter Swierstra

Publication date: 20 October 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_30

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

Executing and verifying higher-order functional-imperative programs in Maude ⋮ Dijkstra and Hoare monads in monadic computation ⋮ Trace-based verification of imperative programs with I/O ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ From Proposition to Program ⋮ A Coq Library for Internal Verification of Running-Times

Uses Software

• Coq
• Haskell
• Ynot

Cites Work

• Unnamed Item
• Unnamed Item
• A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
• Secure Microkernels, State Monads and Scalable Refinement
• Subset Coercions in Coq
• Ynot
• Formal certification of a compiler back-end or
• Polymorphism and separation in hoare type theory
• An axiomatic basis for computer programming

This page was built for publication: A Hoare Logic for the State Monad