Generic weakest precondition semantics from monads enriched with order

DOI10.1016/j.tcs.2015.03.047zbMath1330.68046OpenAlexW1984184513MaRDI QIDQ890376

Ichiro Hasuo

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.047

zbMATH Keywords

coalgebragamenondeterminismalgebraprogram logicmonadprogram verificationeffectcategorical modelprecondition calculus

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) 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) Eilenberg-Moore and Kleisli constructions for monads (18C20)

Related Items

Quantitative logics for equivalence of effectful programs ⋮ Weakest preconditions in fibrations ⋮ Combining algebraic effect descriptions using the tensor of complete lattices ⋮ Up-to techniques for behavioural metrics via fibrations ⋮ Graded algebraic theories ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ Unnamed Item ⋮ Healthiness conditions for predicate transformers ⋮ Combining semilattices and semimodules ⋮ Graded Hoare logic and its categorical semantics ⋮ Up-To Techniques for Behavioural Metrics via Fibrations ⋮ Steps and traces ⋮ Weakest preconditions in fibrations ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Coinductive predicates and final sequences in a fibration
• Identifying all preorders on the subdistribution monad
• Retracted: Semantic domains for combining probability and non-determinism
• Coalgebraic methods in computer science. 12th IFIP WG 1.3 international workshop, CMCS 2014, colocated with ETAPS 2014, Grenoble, France, April 5--6, 2014. Revised selected papers
• Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
• Effect algebras and unsharp quantum logics.
• Coalgebraic semantics of modal logics: an overview
• Notions of computation and monads
• A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language
• Semantics of probabilistic programs
• Structural induction and coinduction in a fibrational setting
• Categorical logic and type theory
• The weakest precondition calculus: Recursion and duality
• Automata, logics, and infinite games. A guide to current research
• Coalgebraic modal logic: soundness, completeness and decidability of local consequence
• Relating computational effects by \(\top \top \)-lifting
• Combining effects: sum and tensor
• Strong functors and monoidal monads
• The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems
• Handling Algebraic Effects
• Complementation of Coalgebra Automata
• The Mathematical Language of Quantum Theory
• New Directions in Categorical Logic, for Classical, Probabilistic and Quantum Logic
• Generic Forward and Backward Simulations II: Probabilistic Simulation
• Coalgebraic Automata Theory: Basic Results
• Neighbourhood Structures: Bisimilarity and Basic Model Theory
• Predicate transformers for extended probability and non-determinism
• Programming as a Discipline of Mathematical Nature
• Preorders on Monads and Coalgebraic Simulations
• Measurable Spaces and Their Effect Logic
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• A Coalgebraic Approach to Linear-Time Logics
• Generic Trace Semantics via Coinduction
• Distributing probability over non-determinism
• An axiomatic basis for computer programming