Graded Hoare logic and its categorical semantics
From MaRDI portal
Publication:2233460
DOI10.1007/978-3-030-72019-3_9zbMATH Open1473.68043arXiv2007.11235OpenAlexW3145817034MaRDI QIDQ2233460FDOQ2233460
Authors: Marco Gaboardi, Shin-ya Katsumata, Tetsuya Sato, Dominic Orchard 
Publication date: 18 October 2021
Abstract: Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.
Full work available at URL: https://arxiv.org/abs/2007.11235
Recommendations
- scientific article; zbMATH DE number 4202247
- Categorical semantics of linear logic
- scientific article; zbMATH DE number 1678378
- scientific article; zbMATH DE number 3875278
- Partial Horn logic and Cartesian categories
- Generalized bounded linear logic and its categorical semantics
- Intermediate logics and categories
- On the categorical semantics of elementary linear logic
- Hybrid Categorial Logics
- scientific article; zbMATH DE number 7599489
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Categorical logic, topoi (03G30)
Cites Work
- Categorical logic and type theory
- Title not available (Why is that?)
- Categories for Types
- Twisted Graded Algebras and Equivalences of Graded Categories
- Title not available (Why is that?)
- Notions of computation and monads
- 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
- Generic models for computational effects
- Construction of biclosed categories
- Logical relations for monadic types
- Hoare Logic in the Abstract
- Probabilistic relational reasoning for differential privacy
- Semantics, logics, and calculi. Essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays
- A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
- Generic weakest precondition semantics from monads enriched with order
- Dijkstra and Hoare monads in monadic computation
- A core quantitative coeffect calculus
- A Hoare-like proof system for analysing the computation time of programs
- Graded algebraic theories
- Title not available (Why is that?)
- A double category theoretic analysis of graded linear exponential comonads
- Title not available (Why is that?)
- Parameterised notions of computation
- Coeffects: a calculus of context-dependent computation
- Approximate relational Hoare logic for continuous random samplings
- Proving differential privacy via probabilistic couplings
- Parametric effect monads and semantics of effect systems
- Generic trace semantics and graded monads
- Combining effects and coeffects via grading
- Bounded Linear Types in a Resource Semiring
- Functors are type refinement systems
- Commutative semantics for probabilistic programming
- Codensity lifting of monads and its dual
- Information Security and Cryptology - ICISC 2005
- Towards a formal theory of graded monads
- Graded monads and rings of polynomials
- Graded Hoare logic and its categorical semantics
- Higher-order approximate relational refinement types for mechanism design and differential privacy
- The sequential semantics of producer effect systems
- Title not available (Why is that?)
- Unifying graded and parameterised monads
- Coeffects: unified static analysis of context-dependence
Cited In (5)
This page was built for publication: Graded Hoare logic and its categorical semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233460)
