Dijkstra and Hoare monads in monadic computation

DOI10.1016/j.tcs.2015.03.020zbMath1330.68047OpenAlexW2127203965MaRDI QIDQ890377

Bart Jacobs

Publication date: 10 November 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.03.020

zbMATH Keywords

Hoare logicmonadprogram semanticsweakest precondition

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15)

Related Items

Unnamed Item ⋮ Graded Hoare logic and its categorical semantics ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Ynot

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Effect algebras and unsharp quantum logics.
• Notions of computation and monads
• Domain theory in logical form
• Categorical logic and type theory
• Semantics of weakening and contraction
• Coreflections in algebraic quantum logic
• Postulates for the barycentric calculus
• From Kleisli Categories to Commutative C *-Algebras: Probabilistic Gelfand Duality
• Dijkstra Monads in Monadic Computation
• Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad
• The Mathematical Language of Quantum Theory
• Convexity, Duality and Effects
• A Hoare Logic for the State Monad
• Ynot
• Formal certification of code-based cryptographic proofs
• Measurable Spaces and Their Effect Logic
• Category Theory
• Quantum weakest preconditions