Graded Hoare logic and its categorical semantics
From MaRDI portal
Publication:2233460
DOI10.1007/978-3-030-72019-3_9zbMath1473.68043arXiv2007.11235OpenAlexW3145817034MaRDI QIDQ2233460
Marco Gaboardi, Shin-ya Katsumata, Tetsuya Sato, Dominic A. Orchard
Publication date: 18 October 2021
Full work available at URL: https://arxiv.org/abs/2007.11235
Logic in computer science (03B70) Categorical logic, topoi (03G30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Indexed and fibered structures for partial and total correctness assertions ⋮ Flexibly graded monads and graded algebras ⋮ Divergences on monads for relational program logics ⋮ Graded Hoare logic and its categorical semantics
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday
- Freyd categories are enriched Lawvere theories
- Notions of computation and monads
- Generic models for computational effects
- Generic weakest precondition semantics from monads enriched with order
- Dijkstra and Hoare monads in monadic computation
- Semantics, logics, and calculi. Essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays
- A Hoare-like proof system for analysing the computation time of programs
- Categorical logic and type theory
- A double category theoretic analysis of graded linear exponential comonads
- Approximate relational Hoare logic for continuous random samplings
- Graded algebraic theories
- Graded Hoare logic and its categorical semantics
- Graded monads and rings of polynomials
- Towards a Formal Theory of Graded Monads
- Coeffects
- Functors are Type Refinement Systems
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
- The sequential semantics of producer effect systems
- Probabilistic relational reasoning for differential privacy
- Combining effects and coeffects via grading
- Commutative Semantics for Probabilistic Programming
- Logical relations for monadic types
- Hoare Logic in the Abstract
- Parameterised notions of computation
- Categories for Types
- Codensity Lifting of Monads and its Dual
- Proving Differential Privacy via Probabilistic Couplings
- Twisted Graded Algebras and Equivalences of Graded Categories
- A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
- Generic Trace Semantics and Graded Monads.
- Coeffects: Unified Static Analysis of Context-Dependence
- Parametric effect monads and semantics of effect systems
- Bounded Linear Types in a Resource Semiring
- A Core Quantitative Coeffect Calculus
- Construction of biclosed categories
- Information Security and Cryptology - ICISC 2005
