Weakest preconditions in fibrations
From MaRDI portal
Publication:2133463
DOI10.1016/j.entcs.2020.09.002OpenAlexW3094043897WikidataQ113317309 ScholiaQ113317309MaRDI QIDQ2133463
Alejandro Aguirre, Shin-ya Katsumata
Publication date: 29 April 2022
Full work available at URL: https://doi.org/10.1016/j.entcs.2020.09.002
Hoare logicmonadcomputational effectsfibered category theoryweakest precondition predicate transformer
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (3)
Indexed and fibered structures for partial and total correctness assertions ⋮ A general semantic construction of dependent refinement type systems, categorically ⋮ Weakest preconditions in fibrations
Cites Work
- Unnamed Item
- 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
- Categorical logic and type theory
- Quantitative logics for equivalence of effectful programs
- Expressivity of coalgebraic modal logic: the limits and beyond
- Strong functors and monoidal 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
- 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
