Graded Hoare logic and its categorical semantics
From MaRDI portal
Publication:2233460
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.
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
Cites work
- scientific article; zbMATH DE number 108368 (Why is no real title available?)
- scientific article; zbMATH DE number 3606647 (Why is no real title available?)
- scientific article; zbMATH DE number 1088046 (Why is no real title available?)
- scientific article; zbMATH DE number 6820296 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- A Hoare-like proof system for analysing the computation time of programs
- A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
- A core quantitative coeffect calculus
- A double category theoretic analysis of graded linear exponential comonads
- A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday
- Approximate relational Hoare logic for continuous random samplings
- Bounded Linear Types in a Resource Semiring
- Categorical logic and type theory
- Categories for Types
- Codensity lifting of monads and its dual
- Coeffects: a calculus of context-dependent computation
- Coeffects: unified static analysis of context-dependence
- Combining effects and coeffects via grading
- Commutative semantics for probabilistic programming
- Construction of biclosed categories
- Dijkstra and Hoare monads in monadic computation
- Freyd categories are enriched Lawvere theories
- Functors are type refinement systems
- Generic models for computational effects
- Generic trace semantics and graded monads
- Generic weakest precondition semantics from monads enriched with order
- Graded Hoare logic and its categorical semantics
- Graded algebraic theories
- Graded monads and rings of polynomials
- Higher-order approximate relational refinement types for mechanism design and differential privacy
- Hoare Logic in the Abstract
- Information Security and Cryptology - ICISC 2005
- Logical relations for monadic types
- Notions of computation and monads
- Parameterised notions of computation
- Parametric effect monads and semantics of effect systems
- Probabilistic relational reasoning for differential privacy
- Proving differential privacy via probabilistic couplings
- Semantics, logics, and calculi. Essays dedicated to Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays
- The sequential semantics of producer effect systems
- Towards a formal theory of graded monads
- Twisted Graded Algebras and Equivalences of Graded Categories
- Unifying graded and parameterised monads
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)
