Weakest preconditions in fibrations
DOI10.1017/S0960129522000330zbMath1506.68053MaRDI QIDQ5058365
Satoshi Kura, Alejandro Aguirre, Shin-ya Katsumata
Publication date: 20 December 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Categorical logic, topoi (03G30) 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) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Notions of computation and monads
- On the relations between monadic semantics
- Generic weakest precondition semantics from monads enriched with order
- Sheaves in geometry and logic: a first introduction to topos theory
- Categorical logic and type theory
- Semantics of weakening and contraction
- Quantitative logics for equivalence of effectful programs
- Weakest preconditions in fibrations
- Indexed and fibred structures for Hoare logic
- The formal theory of monads
- Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
- Functors are Type Refinement Systems
- Logical relations for monadic types
- Hoare Logic in the Abstract
- Guarded commands, nondeterminacy and formal derivation of programs
- Codensity Lifting of Monads and its Dual
- Healthiness from Duality
- Abstraction, Refinement and Proof for Probabilistic Systems
- Traced monoidal categories
- Semantics for Algebraic Operations
- Up-To Techniques for Behavioural Metrics via Fibrations
- Sound Over-Approximation of Probabilities
- Combining probabilistic and non-deterministic choice via weak distributive laws
- Generic Hoare Logic for Order-Enriched Effects with Exceptions
- A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
- Dijkstra monads for free
- Computer Science Logic
- Distributing probability over non-determinism
This page was built for publication: Weakest preconditions in fibrations
