key: cord-0060422-8ke5ufjw
authors: Gaboardi, Marco; Katsumata, Shin-ya; Orchard, Dominic; Sato, Tetsuya
title: Graded Hoare Logic and its Categorical Semantics
date: 2021-03-23
journal: Programming Languages and Systems
DOI: 10.1007/978-3-030-72019-3_9
sha: 8efa0087b3263cd262ec59be88e5473709c150ff
doc_id: 60422
cord_uid: 8ke5ufjw

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.

The paradigm of grading is an emerging approach for augmenting language semantics and type systems with fine-grained information [40] . For example, a graded monad provides a mechanism for embedding side-effects into a pure language, exactly as in the approach of monads, but where the types are augmented ("graded") with information about what effects may occur, akin to a type-and-effect system [24, 42] . As another example, graded comonadic type operators in linear type systems can capture non-linear dataflow and properties of data use [7, 16, 44] . In general, graded types augment a type system with some algebraic structure which serves to give a parameterisable fine-grained program analysis capturing the underlying structure of a type theory or semantics.

Much of the work in graded types has arisen in conjunction with categorical semantics, in which graded modal type operators are modelled via graded monads [13, 17, 25, 36, 33] , graded comonads (often with additional graded monoidal structure) [7, 16, 25, 43, 44] , graded 'joinads' [36] , graded distributive laws between graded (co)monads [15] , and graded Lawvere theories [27] .

So far grading has mainly been employed to reason about functional languages and calculi, thus the structure of the λ-calculus has dictated the structure of categorical models (although some recent work connects graded monads with classical dataflow analyses on CFGs [21] ). We investigate here the paradigm of grading instead applied to imperative languages. As it happens, there is already a healthy thread of work in the literature augmenting program logics (in the family of Floyd-Hoare logics) with analyses that resemble notions of grading seen more recently in the functional world. The general approach is to extend the power of deductive verification by augmenting program logic rules with an analysis of side effects, tracked by composing rules. For example, work in the late 1980s and early 1990s augmented program logics with an analysis of computation time, accumulating a cost measure [37, 38] , with more recent finegrained resource analysis based on multivariate analysis associated to program variables [8] . As another example, the Union Bound Logic of Barthe et al. [5] defines a Hoare-logic-style system for reasoning about probabilistic computations with judgments β c : φ ⇒ ψ for a program c annotated by the maximum probability β (the union bound) that ψ does not hold. The inference rules of Union Bound Logic track and compute the union bound alongside the standard rules of Floyd-Hoare logic. As a last example, Approximate Relational Hoare Logic [2, 6, 39, 48] augments a program logic with measures of the -δ bounds for reasoning about differential privacy.

In this work, we show how these disparate approaches can be unified by adapting the notion of grading to an imperative program-logic setting, for which we propose Graded Hoare Logic (GHL): a parameterisable program logic and reasoning framework graded by a preordered monoidal analysis. Our core contribution is GHL's underlying semantic framework which integrates grading, logical assertions (pre-and post-conditions) and the effectful semantics of an imperative language. This framework allows us to model, in a uniform way, the different augmented program logics discussed above.

Graded models of functional calculi tend to adopt either a graded monadic or graded comonadic model, depending on the direction of information flow in the analysis. We use the opportunity of an imperative setting (where the λ-calculus' asymmetrical 'many-inputs-to-one-output' model is avoided) to consider a more flexible semantic basis of graded categories. Graded categories generalise graded (co)monadic approaches, providing a notion of graded denotation without imposing on the placement (or 'polarity') of grading.

Outline Section 2 begins with an overview of the approach, focusing on the example of Union Bound Logic and highlighting the main components of our semantic framework. The next three sections then provide the central contributions:

-Section 3 defines GHL and its associated assertion logic which provides a flexible, parameterisable program logic for integrating different notions of side-effect reasoning, parameterised by a preordered monoidal analysis. We instantiate the program logic to various examples. -Section 4 explores graded categories, an idea that has not been explored much in the literature, and for which there exists various related but not-quiteoverlapping definitions. We show that graded categories can abstract graded monadic and graded comonadic semantics. We then extend graded categories to Freyd categories (generally used as a more flexible model of effects than monads), introducing the novel structure of graded Freyd categories. -Section 5 develops the semantic framework for GHL, based on graded Freyd categories in a fibrational setting (where coherent fibrations [22] model the assertion logic) integrated with the graded Freyd layer. We instantiate the semantic model to capture the examples presented in Section 3 and others drawn from the literature mentioned above.

An extended version of this paper provides appendices which include further examples and proof details [14] .

As discussed in the introduction, several works explore Hoare logics combined with some form of implicit or explicit grading for program analysis. Our aim is to study these in a uniform way. We informally introduce of our approach here. We start with an example which can be derived in Union Bound Logic [5] :

This judgment has several important components. First, we have primitives for procedures with side-effects such as do v 1 ← Gauss(0, 1). This procedure samples a random value from the standard normal distribution with mean 0 and variance 1 and stores the result in the variable v 1 . This kind of procedure with side effects differs from a regular assignment such as v := max(v 1 , v 2 ), which is instead considered to be pure (wrt. probabilities) in our approach. The judgment has grade '0.05' which expresses a bound on the probability that the postcondition is false, under the assumption of the precondition, after executing the program; we can think of it as the probability of failing to guarantee the postcondition. In our example (call it program P ), since the precondition is true, this can be expressed as: Pr P (m) [v > 2] ≤ 0.05 where P (m) is the probability distribution generated in executing the program. The grade of P in this logic is derived using three components. First, sequential composition:

which sums the failure probabilities. Second, an axiom for Gaussian distribution:

with a basic constant 0.025 which comes from the property of the Gaussian distribution we are considering. Third, by the following judgment which is derivable by the assignment and the consequence rules, which are the ones from Hoare Logic with a trivial grading 0 which is the unit of addition:

Judgments for more complex examples can be derived using the rules for conditional and loops. These rules also consider grading, and the grading can depend on properties of the program. For example the rule for conditionals is:

This allows one to reason also about the grading in a conditional way, through the two assumptions ψ ∧ e b = tt and ψ ∧ e b = ff. We give more examples later.

Other logics share a similar structure as that described above for the Union Bound logic, for example the relational logic apRHL [2] , and its variants [48, 49] , for reasoning about differential privacy. Others again use a similar structure implicitly, for example the Hoare Logic to reason about asymptotic execution cost by Nielson [37] , Quantitative Hoare Logic [8] , or the relational logic for reasoning about program counter security presented by Barthe [3] .

To study the semantics of these logics in a uniform way, we first abstract the logic itself. We design a program logic, which we call Graded Hoare Logic (GHL), containing all the components discussed above. In particular, the language is a standard imperative language with conditional and loops. Since our main focus is studying the semantics of grading, for simplicity we avoid using a 'while' loop, using instead a bounded 'loop' operation (loop e do P ). This allow us to focus on the grading structures for total functions, leaving the study of the interaction between grading and partiality to future work. The language is parametric in the operations that are supported in expressions-common in several treatments of Hoare Logic-and in a set of procedures and commands with side effects, which are the main focus of our work. GHL is built over this language and an assertion logic which is parametric in the basic predicates that can be used to reason about programs. GHL is also parametric in a preordered monoid of grades, and in the axioms associated with basic procedures and commands with side effects. This generality is needed in order to capture the different logics we mentioned before.

GHL gives us a unified syntax, but our real focus is the semantics. To be as general as possible we turn to the language of category theory. We give a categorical framework which can capture different computational models and side effects, with denotations that are refined by predicates and grades describing program behaviours. Our framework relates different categories (modelling different aspects of GHL) as summarized by the following informal diagram (1).

This diagram should not be understood as a commutative diagram in CAT as E is a graded category and hence not an object of CAT.

The category V models values and pure computations, the category C models impure computations, P is a category of predicates, and E is a graded category whose hom-sets are indexed by grades-elements of a preordered monoid. The presentation of graded categories is new here, but has some relation to other structures of the same name (discussed in Section 4).

This diagram echos the principle of refinement as functors proposed by Melliès and Zeilberger [32] . The lower part of the diagram offers an interpretation of the language, while the upper part offers a logical refinement of programs with grading. However, our focus is to introduce a new graded refinement view. The ideas we use to achieve this are to interpret the base imperative language using a Freyd category I : V → C (traditionally used to model effects) with countable coproducts, to interpret the assertion logic with a coherent fibration p : P → V, and to interpret GHL as a graded Freyd categoryİ : P → E with homogeneous coproducts. In addition, the graded category E has a functor 5 q into C which erases assertions and grades and extracts the denotation of effectful programs, in the spirit of refinements. The benefit of using a Freyd category as a building block is that they are more flexible than other structures (e.g., monads) for constructing models of computational effects [47, 51] . For instance, in the category Meas of measurable spaces and measurable functions, we cannot define state monads since there are no exponential objects. However, we can still have a model of first-order effectful computations using Freyd categories [46] .

Graded Freyd categories are a new categorical structure that we designed for interpreting GHL judgments (Section 4.2). The major difference from an ordinary Freyd category is that the 'target' category is now a graded category (E in the diagram (1)). The additional structure provides what we need in order to interpret judgments including grading.

To show the generality of this structure, we present several approaches to instantiating the categorical framework of GHL's semantics, showing constructions via graded monads and graded comonads preserving coproducts.

Part of the challenge in designing a categorical semantics for GHL is to carve out and implement the implicit assumptions and structures used in the semantics of the various Hoare logics. A representative example of this challenge is the interpretation of the rule for conditionals in Union Bound Logic that we introduced above. We interpret the assertion logic in (a variant of) coherent fibrations p : P → V, which model the ∧∨∃=-fragment of first-order predicate logic [22] . In this abstract setup, the rule for conditionals may become unsound as it is built on the implicit assumption that the type Bool, which is interpreted as 1 + 1, consists only of two elements, but this may fail in general V. For example, a suitable coherent fibration for relational Hoare logic would take Set 2 as the base category, but we have Set 2 (1, 1+1) ∼ = 4, meaning that there are four global elements in the interpretation of Bool. We resolve this problem by introducing a side condition to guarantee the decidability of the boolean expression:

This is related to the synchronization condition appearing in the relational Hoare logic rule for conditional commands (e.g., [6] ).

Another challenge in the design of the GHL is how to assign a grade to the loop command loop e do P . We may naïvely give it the grade m l i∈N m i , where m is the grade of P , because P is repeatedly executed some finite number of times. However, the grade m l is a very loose over-approximation of the grade of loop e do P . Even if we obtain some knowledge about the iteration count e in the assertion logic, this cannot be reflected in the grade. To overcome this problem, we introduce a Hoare logic rule that can estimate a more precise grade of loop e do P , provided that the value of e is determined:

This rule brings together the assertion language and grading, creating a dependency from the former to the latter, and giving us the structure needed for a categorical model. The right premise is a judgment of the assertion logic (under program variables Γ M and pre-condition ψ N ) requiring that e is statically determinable as N . This premise makes the rule difficult to use in practical applications where e is dynamic. We expect a more "dependent" version of this rule is possible with a more complex semantics internalizing some form of datadependency. Nevertheless, the above is enough to study the semantics of grading and its interaction with the Hoare Logic structure, which is our main goal here.

After introducing some notation and basic concepts used throughout, we outline a core imperative loop language, parametric in its set of basic commands and procedures (Section 3.2). We then define a template of an assertion logic (Section 3.3), which is the basis of Graded Hoare Logic (Section 3.4).

Throughout, we fix an infinite set Var of variables which are employed in the loop language (as the names of mutable program variables) and in logic (to reason about these program variables). Let Σ = (S, · · · ) be a many-sorted signature. A context for Σ is a (possibly empty) sequence of pairs Γ ∈ (Var×S) * such that all variables in Γ are distinct. We regard Γ as a partial mapping from Var to S. The set of contexts for Σ is denoted Ctx Σ . For s ∈ S and Γ ∈ Ctx Σ , we denote by Exp Σ (Γ, s) the set of Σ-expressions of sort s under the context Γ . When Σ, Γ are obvious, we simply write e : s to mean e ∈ Exp Σ (Γ, s). This set is inductively defined as usual.

An interpretation of a many-sorted signature Σ = (S, O, ar) in a cartesian category (V, 1, ×) consists of an assignment of an object [[s]] ∈ V for each sort s ∈ S and an assignment of a morphism

. . , s n , s . Once such an interpretation is given, we extend it to Σ-expressions in the standard way (see, e.g. [9, 45] 

Throughout, we write bullet-pointed lists marked with for the mathematical data that are parameters to Graded Hoare Logic (introduced in Section 3.4).

We introduce an imperative language called the loop language, with a finite looping construct. The language is parameterised by the following data: a many-sorted signature Σ = (S, O, ar) extending a base signature (S 0 , O 0 , ar 0 ) of sort S 0 = {bool, nat} with essential constants as base operators O 0 , shown here with their signatures for brevity rather than defining ar 0 directly:

where bool is used for branching control-flow and nat is used for controlling loops, whose syntactic constructs are given below. We write k to mean the embedding of semantic natural numbers into the syntax. a set CExp of command names (ranged over by c) and a set PExp s of procedure names of sort s (ranged over by p) for each sort s ∈ S.

When giving a program, we first fix a context Γ M for the program variables. We define the set of programs (under a context Γ M ) by the following grammar:

where v ∈ Γ M , e b , e n are well-typed Σ-expressions of sort bool and nat under Γ M , and c ∈ CExp. In assignment commands, e ∈ Exp Σ (Γ M , Γ (v)). In procedure call commands, p ∈ PExp Γ (v) . Each program must be well-typed under Γ M . The typing rules are routine so we omit them.

Thus, programs can be sequentially composed via ; with skip as the trivial program which acts as a unit to sequencing. An assignment v := e assigns expressions to a program variable v. Commands can be executed through the instruction do c which yields some side effects but does not return any value.

Procedures can be executed through a similar instruction do v ← p which yields some side effect but also returns a value which is used to update v. Finally, conditionals are guarded by a boolean expression e b and the iterations of a looping construct are given by a natural number expression e n (which is evaluated once at the beginning of the loop to determine the number of iterations).

This language is rather standard, except for the treatment of commands and procedures of which we give some examples here.

Example 1. Cost Information: a simple example of a command is tick, which yields as a side effect the recording of one 'step' of computation.

Control-Flow Information: two other simple example of commands are cfTT and cfFF, which yield as side effects the recording of either true or false to a log. A program can be augmented with these commands in its branches to give an account of a program's control flow. We will use these commands to reason about control-flow security in Example 3.

Probability Distributions: a simple example of a procedure is Gauss(x, y), which yields as a side effect the introduction of new randomness in the program, and which returns a random sample from the Gaussian distribution with mean and variance specified by x, y ∈ Γ M . We will see how to use this procedure to reason about probability of failure in Example 4.

Concrete instances of the loop language typically include conversion functions between the sorts in Σ, e.g., so that programs can dynamically change control flow depending on values of program variables. In other instances, we may have a language manipulating richer data types, e.g., reals or lists, and also procedures capturing higher-complexity computations, such as Ackermann functions.

We use an assertion logic to reason about properties of basic expressions. We regard this reasoning as a meta-level activity, thus the logic can have more sorts and operators than the loop language. Thus, over the data specifying the loop language, we build formulas of the assertion logic by the following data: a many-sorted signature Σ l = (S l , O l , ar l ) extending Σ. a set P l of atomic propositions and a function par l : P l → S * l assigning input sorts to them. We then inductively define the set Fml Σ l (Γ ) of formulas under Γ ∈ Ctx Σ l as in Figure 1 (over the page), ranged over by ψ and φ.

The assertion logic is a fragment of the many-sorted first-order logic over Σ lterms admitting: 1) finite conjunctions, 2) countable disjunctions, 3) existential quantification, and 4) equality predicates. Judgements in the assertion logic have the form Γ | ψ 1 , · · · , ψ n φ (read as ψ 1 ∧ · · · ∧ ψ n implies φ), where Γ ∈ Ctx Σ l is a context giving types to variables in the formulas ψ 1 , · · · , ψ n , φ ∈ Fml Σ l (Γ ). The logic has the axiom rule deriving Γ | ψ φ for each pair (ψ, φ) of formulas in Axiom(Γ ). The rest of inference rules of this logic are fairly standard and so we omit them (see e.g. [22, Section 3.2 and Section 4.1]).

The set FmlΣ l (Γ ) of formulas under Γ ∈ CtxΣ l is inductively defined as follows:

1. For all p ∈ P l and par l (p) = s1 · · · sn and ti :

3. For all finite families {φi ∈ FmlΣ l (Γ )}i∈Λ, we have φi ∈ FmlΣ l (Γ ). 4. For all countable families {φi ∈ FmlΣ l (Γ )}i∈Λ, we have φi ∈ FmlΣ l (Γ ). 5. For all φ ∈ FmlΣ l (Γ, x : s), we have (∃x : s . φ) ∈ FmlΣ l (Γ ).

In some of our examples we will use the assertion logic to reason about programs in a relational way, i.e., to reason about two executions of a program (we call them left and right executions). This requires basic predicates to manage expressions representing pairs of values in our assertion logic. As an example, we could have two predicates eqv 1 , eqv 2 , that can assert the equality of the left and right executions of an expression to some value, respectively. That is, the formula eqv 1 (e b , true), which we will write using infix notation e b 1 = true, asserts that the left execution of the boolean expression e b is equal to true.

We now introduce Graded Hoare Logic (GHL), specified by the following data: a preordered monoid (M, ≤, 1, ·) (pomonoid for short) (where · is monotonic with respect to ≤) for the purposes of program analysis, where we refer to the elements m ∈ M as grades; two functions which define the grades and pre-and post-conditions of commands CExp and procedures PExp:

The function C c takes a pre-condition and a grade, returning a set of command symbols satisfying these specifications. A command c may appear in C c (φ, m) for different pairs (φ, m), enabling pre-condition-dependent grades to be assigned to c. Similarly, the function C s p takes a pre-condition, a grade, and a postcondition for return values, and returns a set of procedure names of sort s satisfying these specifications. Note, r is a distinguished variable (for return values) not in Γ M . The shape of C c and C c as predicates over commands and procedures, indexed by assertions and grades, provides a way to link grades and assertions for the effectful operations of GHL. Section 3.5 gives examples exploiting this.

From this structure we define a graded Hoare logic by judgments of the form:

and analysis m ∈ M . Graded judgments are defined inductively via the inference rules given in Table 1 . Ignoring grading, many of the rules are fairly standard for a Floyd-Hoare program logic. The rule for skip is standard but includes grading by the unit 1 of the monoid. Similarly, assignment Table 1 . Graded Hoare Logic Inference Rules is standard, but graded with 1 since we do not treat it specially in GHL. Sequential composition takes the monoid multiplication of the grades of the subterms. The rules for commands and procedures use the functions C c and C p introduced above. Notice that the rule for commands uses as the pre-condition as its postcondition, since commands have only side effects and they do not return any value. The rule for procedures combines the pre-and post-conditions given by C p following the style of Floyd's assignment rule [12] .

The non-syntax-directed consequence rule is similar to the usual consequence rule, and in addition allows the assumption on the grade to be weakened (approximated ) according to the ordering of the monoid.

The shape of the loop rule is slightly different from the usual one. It uses the assertion-logic judgment Γ M | ψ N e n = N to express the assumption that e n evaluates to N . Under this assumption it uses a family of assertions ψ z indexed by the natural numbers z ∈ {0, 1, . . . , N − 1} to conclude the post-condition ψ 0 . This family of assertions plays the role of the classical invariant in the Floyd-Hoare logic rule for 'while'. Assuming that the grade of the loop body is m, the grade of the loop command is then m N , where m 0 = 1 and m k+1 = m · m k . By instantiating this rule with ψ z = (θ ∧ e n = z ), the loop rule also supports the following derived rule which is often preferable in examples:

The rule for the conditional is standard except for the condition Γ M | ψ e b = tt ∨ e b = ff. While this condition may seem obvious, it is actually important to make GHL sound in various semantics (mentioned in Section 2). As an example, suppose that a semantics [[−]] of expressions is given in the product category Set 2 , which corresponds to two semantics [

Then the side condition for the conditional is to guarantee that for any boolean expression e b , and pair of memories (ρ 1 , ρ 2 ) satisfying the precondition ψ, the pair

. We note that other relational logics such as apRHL [6] employ an equivalent syntactic side condition in their rule for conditionals.

Example 2 (Simple cost analysis). We can use the tick command discussed in Example 1 to instrument programs with cost annotations. We can then use GHL to perform cost analysis by instantiating GHL with the additive natural number monoid (N, ≤, 0, +) and tick ∈ C c (φ, 1). Thus, we can form judgments 1 {φ} do tick {φ} which account for cost via the judgment's grade. Sequential composition accumulates cost and terms like skip and assignment have 0 cost. Let us use this example to illustrate how C c can assign multiple pre-conditiongrade pairs to a command. Suppose that we modify the semantics of tick so that it reports unit cost 1 when variable x is 0, otherwise cost 2. We can then define C c so that tick ∈ C c (x = 0 , 1) and also tick ∈ C c (x = 0 , 2). In this way, we can give different grades to programs depending on their pre-conditions.

We can use the commands cfTT and cfFF discussed in Example 1 to instrument programs with control flow annotations, recording to an external log. GHL can then be used to reason about program counter security [35] [3, Section 7.2] of instrumented programs. This is a relational security property similar to non-interference (requiring that private values do not influence public outputs) but where only programs with the same control flow are considered.

Firstly, any conditional statement if e b then P t else P f in a program is elaborated to a statement if e b then (cfTT; P t ) else (cfFF; P f ). We then instantiate GHL with a monoid of words over {tt, ff} with prefix order: 2 * ({tt, ff} * , ≤ , , ·) and we consider cfTT ∈ C c (φ, tt) and cfTT ∈ C c (φ, ff). We can thus form judgments of the shape tt {φ} do cfTT {φ} and ff {φ} do cfFF {φ} which account for control-flow information (forming paths) via the judgment's grade. Sequential composition concatenates control-flow paths and terms like skip and assignment do not provide any control-flow information, i.e. .

We then instantiate the assertion logic to support relational reasoning, i.e., where the expressions of the language are interpreted as pair of values. For an expression e, interpreted as a pair (v 1 , v 2 ) then we write e 1 = v 1 to say that the first component (left execution) equals v 1 and e 2 = v 2 to say that the second component (right execution) equals v 2 . In the assertion logic, we can then describe public values which need to be equal, following the tradition in reasoning about non-interference, by the predicate e 1 = e 2 . Private data are instead interpreted as a pair of arbitrary values. (Section 3.3 suggested the notation eqv i (e, b) for e i = b, but we use the latter for compactness here).

As an example, one can prove the following judgment where x is a public variable and y is a private one, and b ∈ {tt, ff}: b {x 1 =x 2 ∧x 1 =b}if x then (cfTT; x=1; y=1) else (cfFF; x=2; y=2){x 1 =x 2 } This judgment shows the program is non-interferent, since the value of x is independent from the value of the private variable y, and secure in the program counter model, since the control flow does not depend on the value of y. Conversely, the following judgment is not derivable for both b = tt and b = ff: b {x 1 =x 2 ∧y 1 =b}if y then (cfTT; x=1; y=1) else (cfFF; x=1; y=2){x 1 =x 2 } This program is non-interferent but is not secure in the program counter model because the control flow leaks information about y which is a private variable.

Example 4 (Union Bound Logic). Section 1 discussed the Union Bound logic by Barthe et al. [5] . This logic embeds smoothly into GHL by using the pomonoid (R ≥0 , ≤, 0, +) and procedures of the form sample μ,e as samplings from a probabilistic distribution μ parametrised over the syntax of GHL expressions e. Following Barthe et al. [5] , we consider a semantically defined set for C p :

This definition captures that, assuming the pre-condition holds for an input memory state s, then for output value s from sampling sample μ,e , the probability that the post-condition is false is bounded above by β. This allow us to consider different properties of the distribution μ with parameter e.

Now that we have introduced GHL and key examples, we turn to the core of its categorical semantics: graded categories.

Graded monads provide a notion of sequential composition for morphisms of the form I → T m J, i.e., with structure on the target/output capturing some information by the grade m drawn from a pomonoid [24] ; dually, graded comonads provide composition for D m I → J, i.e. with structure on the source/input with grade m [43]. We avoid the choice of whether to associate grading with the input or output by instead introducing graded categories, which are agnostic about the polarity (or position) of any structure and grading. Throughout this section, we fix a pomonoid (M, ≤, 1, ·) (with · monotonic wrt. ≤). Graded categories satisfy the usual categorical laws of identity and associativity, and also the commutativity of upcast and composition: ↑ n n g•↑ m m f = ↑ m ·n m·n (g•f ), corresponding to monotonicity of (·) with respect to ≤.

An intuitive meaning of a graded category's morphisms is: f ∈ C(A, B)(m) if the value or the price of a morphism f : A → B is at most m with respect to the ordering ≤ on M . We do not yet give a polarity or direction to this price, i.e., whether the price is consumed or produced by the computation. Thus, graded categories give a non-biased view; we need not specify whether grading relates to the source or target of a morphism.

Graded categories were first introduced by Wood [54, Section 1] (under the name 'large V -categories'), and Levy connected them with models of call-bypush-value [28] . Therefore we do not claim the novelty of Definition 1. They satisfy the graded versions of the usual monad axioms: 

The dual construction is possible. Let D be an M op -graded comonad on a category C. We then define C D by C D (X, Y )(m) = C(DmX, Y ); the rest of data is similar to the case of graded monads. This yields an M -graded category C D .

As an aside (included for completeness but not needed in the rest of the paper), graded categories are an instance of enriched categories. For the enriching category, we take the presheaf category [M, Set], together with Day's convolution product [10] .

We model boolean values and natural numbers by the binary coproduct 1 + 1 and the countable coproduct i∈N 1. We thus define what it means for a graded category to have coproducts. The following definition of binary coproducts easily extends to coproducts of families of objects.

Let C be an M -graded category. A homogeneous binary coproduct of X 1 , X 2 ∈ C consists of an object Z ∈ C together with injections ι 1 ∈ C(X 1 , Z)(1) and ι 2 ∈ C(X 2 , Z)(1) such that, for any m ∈ M and Y ∈ C, the function λf .

The inverse is called the cotupling and denoted by [−, −]. It satisfies the usual law of coproducts (i = 1, 2):

When homogeneous binary coproducts of any combination of X 1 , X 2 ∈ C exists, we say that C has homogeneous binary coproducts.

The difference between homogeneous coproducts and coproducts in ordinary category theory is that the cotupling is restricted to take morphisms with the same grade. A similar constraint is seen in some effect systems, where the typing rule of conditional expressions require each branch to have the same effect. Proposition 1. Let {ι i ∈ C(X i , Z)} i∈I be a coproduct of {X i } i∈I in an ordinary category C.

is a homogeneous coproduct in C T . 2. Suppose that (D, ε, δ) is an M op -graded comonad on C such that each Dm :

C → C preserves the coproduct {ι i } i∈I . Then {ι i • ε I ∈ C D (X i , Z)(1)} i∈I is a homogeneous coproduct in C D .

We now introduce the central categorical structure of the loop language and GHL semantics: graded Freyd categories with homogeneous countable coproducts. The function I and ( * ) satisfy the following equations:

These are analogous to the usual Freyd categories axioms. We also require that:

is a homogeneous countable coproduct.

We denote an M -graded Freyd category with countable coproducts by the tuple (V, 1, ×, C, I, ( * )) capturing the main details of the cartesian monoidal structure of V, the base category C, the lifting function I and the action ( * ).

If the grading pomonoid M is trivial, C becomes an ordinary category with countable coproducts. We therefore simply call it a Freyd category with countable coproducts. This is the same as a distributive Freyd category in the sense introduced by Power [46] and Staton [51] . We will use non-graded Freyd categories to give a semantics of the loop language in Section 4.3. An advantage of Freyd categories is that they encompasses a broad class of models of computations, not limited to those arising from monads. A recent such example is Staton's category of s-finite kernels [52] 7 . We could give an alternative abstract definition of M -graded Freyd category using 2-categorical language: a graded Freyd category is an equivariant morphism in the category of actions from a cartesian category to M -graded categories. The full detail of this formulation will be discussed elsewhere.

A Freyd category typically arises from a strong monad on a cartesian category [47] . We give here a graded analogue of this fact. First, we recall the notion of strength for graded monads [ We often use the following 'ext' operation to structure interpretations of programs and GHL derivations. Let δ X ∈ V(X, X × X) be the diagonal morphism.

Then ext :

When viewing X as a set of environments, ext(f ) may be seen as executing an effectful procedure f under an environment, then extending the environment with the return value of f . In a non-graded setting, the definition of ext is analogous.

Towards the semantics of GHL, we first give a more standard, non-graded categorical semantics of the loop language. We first prepare the following data.

A Freyd category (V, 1, ×, C, I, * ) with countable coproducts. A coproduct {tt, ff ∈ V(1, Bool)} of 1 and 1 in V. Nat) . 

which updates the memory configuration at variable v with the value of e.

For the interpretation of conditional and loop commands, we need coproducts over M. Since V is distributive, we can form a binary coproduct M × Bool and a countable coproduct M × Nat with injections respectively defined as (∀k ∈ N):

By Condition 1 of Definition 3, these coproducts are mapped to coproducts in C with injections: Thus, the semantics of loop e n doP is such that, if the expression e n evaluates to some natural number k then loop e n doP is equivalent to the k-times sequential composition of P .

We now define the categorical model of GHL, building on the non-graded Freyd semantics of Section 4.3. Section 5.1 first models the base assertion logic, for which we use fibrations, giving an overview of the necessary mathematical machinery for completeness. Section 5.2 then defines the semantics of GHL and Section 5.3 instantiates it for the examples discussed previously in Section 3.

Our assertion logic (Section 3) has logical connectives of finite conjunctions, countable disjunctions, existential quantification and an equality predicate. A suitable categorical model for this fragment of first-order logic is offered by a coherent fibration [22, Def. 4.2.1] , extended with countable joins in each fibre. We recap various key definitions and terminology due to Jacobs' textbook [22] . In the following, let P and V be categories and p : P → V a functor. We can regard functor p as attaching predicates to each object in V. When pψ = X, we regard ψ ∈ P as a predicate over X ∈ V. When f ∈ P(ψ, φ) is a morphism, we regard this as saying that pf maps elements satisfying ψ to those satisfying φ in V. Parallel to this view of functors assigning predicates is the notion that entities in P are 'above' those in V when they are mapped to by p.

). An object ψ ∈ P is said to be above an object X ∈ V if pψ = X. Similarly, a morphism 8ḟ ∈ P(ψ, φ) is said to be above a morphism f in V if pḟ = f ∈ V(pψ, pφ). A morphism in P is vertical if it is above an identity morphism. Given ψ, φ ∈ P and f ∈ V(pψ, pφ), then we denote the set of all morphisms in P above f as P f (ψ, φ) = {ḟ ∈ P(ψ, φ) | pḟ = f }.

A fibre category over X ∈ V is a subcategory of P consisting of objects above X and morphisms above id X . This subcategory is denoted by P X , and thus the homsets of P X are P X (ψ, φ) = P id X (ψ, φ).

We are ready to recall the central concept in fibrations: cartesian morphisms. Definition 6 (Cartesian morphism). A morphismḟ ∈ P(ψ, φ) is cartesian if for any α ∈ P and g ∈ V(pα, pψ), the post-composition ofḟ in P, regarded as a function of typeḟ • − : P g (α, ψ) → P g•pḟ (α, φ) , is a bijection. This amounts to the following universal property of cartesian morphism: for anyḣ ∈ P(α, φ) above g • pf , there exists a unique morphismġ ∈ P(α, ψ) above g such thaṫ h =ḟ •ġ. Intuitively,ḟ represents the situation where ψ is a pullback or inverse image of φ along pḟ , and the universal property corresponds to that of pullback.

Finally, a functor p : P → V is a fibration if for any ψ ∈ P, X ∈ V, and f ∈ V(X, pψ), there exists an object φ ∈ P and a cartesian morphismḟ ∈ P(φ, ψ) above f , called the cartesian lifting of f with ψ. We say that a fibration p : P → V is posetal if each P X is a poset, corresponding to the implicational order between predicates. When ψ ≤ φ holds in P X , we denote the corresponding vertical morphism in P as ψ φ.

Posetal fibrations are always faithful. The cartesian lifting of f ∈ V(X, pψ) with ψ uniquely exists. We thus write it by fψ, and its domain by f * ψ. It can be easily shown that for any morphism f ∈ V(X, Y ) in V, the assignment ψ ∈ P Y → f * ψ ∈ P X extends to a monotone function f * : P Y → P X . We call it the reindexing function (along f ). Furthermore, the assignment f → f * satisfies the (contravariant) functoriality: id * X = id P X and (g •f ) * = f * •g * . A fibration is a bifibration if each reindexing function f * : P Y → P X for f ∈ V(X, Y ) has a left adjoint, denoted by f * : P X → P Y . f * ψ is always associated with a morphism f ψ : f * ψ → ψ above f , and this is called the opcartesian lifting of f with ψ. For the universal property of the opcartesian lifting, see Jacobs [22, Def. 9.1.1] .

It is widely known that coherent fibrations are suitable for interpreting the ∧, ∨, ∃, =-fragment of first-order logic (see [22, Chapter 4, Def. 4.2.1]). Based on this fact, we introduce a class of fibrations that are suitable for our assertion logic-due to the countable joins of the assertion logic we modify the definition of coherent fibration accordingly.

A fibration for assertion logic over V is a posetal fibration p : P → V for cartesian V with distributive countable coproducts, such that:

1. Each fibre poset P X is a distributive lattice with finite meets X , ∧ and countable joins ⊥ X , ∨. 2. Each reindexing function f * preserves finite meets and countable joins. 3. The reindexing function c * X,Y along the contraction c X,Y π 1 , π 2 , π 2 ∈ V(X × Y, X × Y × Y ) has a left adjoint Eq X,Y c * X,Y . This satisfies Beck-Chevalley condition and Frobenius property; we refer to [22, Definition 3.4 .1].

4. The reindexing function w * X,Y along the weakening w X,Y π 1 ∈ V(X ×Y, X) has a left adjoint ∃ X,Y w * X,Y . This satisfies Beck-Chevalley condition and Frobenius property; we refer [22, Definition 1.9.1, 1.9.12]. This is almost the same as the definition of coherent fibrations [22, Definition 4.2.1] ; the difference is that 1) the base category V has countable coproducts 2) we require each fibre to be a poset; this makes object equalities hold on-the-nose, and 3) we require each fibre to have countable joins. They will be combined with countable coproducts of V to equip P with a countable coproduct [22] . Example 6. A typical example of a fibration for assertion logic is the subobject fibration p Set : Pred → Set; the category Pred has objects pairs (X, ψ) of sets such that ψ ⊆ X, and morphisms of type (X, ψ) → (Y, φ) as functions f : X → Y such that f (ψ) ⊆ φ. The functor p sends (X, ψ) to X and f to itself. More examples can be found in the work of Jacobs [22, Section 4] .

For a parallel pair of morphisms f, g ∈ V(X, Y ), we define the equality predicate Eq(f, g) above X to be id X , f, g * Eq X,Y ( X×Y ) [22, Notation 3.4.2] . Intuitively, Eq(f, g) corresponds to the predicate {x ∈ X | f (x) = g(x)}. In this paper, we will use some facts about the equality predicate shown by Jacobs [ 

We finally introduce the semantics of Graded Hoare logic. This semantics interprets derivations of GHL judgements m {ψ} P {φ} as m-graded morphisms in a graded category. Moreover, it is built above the interpretation [[P ]] ∈ C(M, M) of the program P in the non-graded semantics introduced in Section 4.3. The underlying structure is given as a combination of a fibration for the assertion logic and a graded category over C, as depicted in (1) (Section 2, p. 237).

A GHL structure over a Freyd category (V, 1, ×, C, I, * ) with countable coproducts and a fibration p : P → V for assertion logic comprises:

1. An M -graded Freyd category (P,1,×, E,İ, ) with homogeneous countable coproducts. 2. A function q ψ,φ,m : E(ψ, φ)(m) → C(pψ, pφ) (subscripts may be omitted), which maps to the base denotational model, erasing assertions and grades.

The above data satisfy the following properties:

1. That q behaves 'functorialy' preserving structure from E to V:

The last statement asserts that if the precondition is the least element ⊥ X in the fibre over X ∈ V, which represents the false assertion, we trivially conclude any postcondition φ and grading m for any morphisms of type X → pφ in C.

The semantics of GHL then requires a graded Freyd category with countable coproducts, and morphisms in the graded category guaranteeing a sound model of the effectful primitives (commands/procedures), captured by the data:

A GHL structure (P,1,×, E,İ, , q) over the Freyd category (V, 1, ×, C, I, * ) with countable coproducts and the fibration p : P → V for assertion logic. The above interpretations largely follow the form of the underlying model of Section 4.3, with the additional information and underlying categorical machinery for grades and assertions here; we now map to E. The interpretation of conditional and loop commands requires some more reasoning.

Conditionals Let p 1 , p 2 be the interpretations of each branch of the conditional command:

We consider the cocartesian lifting id M ,

We name its codomain Im. Next, cartesian morphisms tm(Im) : tm * Im → Im and fm(Im) : fm * Im → Im in P are above the coproduct (M × Bool, tm, fm) in V. Then the interpretations of the preconditions of P 1 , P 2 are inverse images of Im along tm, fm : M → M × Bool:

The side condition of the conditional rule ensures that (Im, tm(Im), fm(Im)) is a coproduct in P:

Therefore the image of the coproduct (Im, tm(Im), fm(Im)) byİ yields a homogeneous coproduct in E. We take the cotupling [p 1 , p 2 ] ∈ E(Im, [[φ]])(m) with respect to this homogeneous coproduct. We finally define the interpretation of the conditional rule to be the following composite:

Loops Fix N ∈ N, and suppose that m {ψ i+1 } P {ψ i } is derivable in the graded Hoare logic for each 0 ≤ i < N.

. We then define a countable family of morphisms (we use here ex falso quodlibet):

. We then send the coproduct θ i → i∈N θ i byİ and obtain a homogeneous coproduct in E. 

We first present a construction of GHL structures from graded monad liftings, which are a graded version of the concept of monad lifting [11, 19, 26] . Before seeing examples, we introduce a notation and fibrations for the assertion logic. Let p : P → V be a fibration for the assertion logic. Below we use the following notation: for f ∈ V(I, J) and ψ ∈ P I and φ ∈ P J , by f : ψ→ φ we mean the statement "there exists a morphismḟ ∈ P(ψ, φ) such that pḟ = f ". Suchḟ is unique due to the faithfulness of p : P → V.

To derive the GHL structure suitable for the semantics of the Union Bound Logic discussed in Example 4, we invoke Theorem 2 by letting p be p Set : Pred → Set (Example 6), T be the subdistribution monad D andṪ be the strong (R ≥0 , ≤, 0, +)-graded lifting U of D defined by U (δ)(X, P ) (D(X), {d | d(X \ P ) ≤ δ}). The induced GHL structure is suitable for the semantics of GHL for Union Bound Logic in Example 4. The soundness of inference rules follow from the GHL structure as we have showed in Section 5.2. To complete the semantics of GHL for the Union Bound Logic, we give the semantics p of procedures p ∈ C s p . Example 4 already gave a semantic condition for these operators: -The category ERel of endorelations defined as follows: an object (X, R) is a pair of X ∈ Set and R ⊆ X × X (i.e. an endorelation R on X) and an arrow f :

The fibration for the assertion logic e : ERel → Set given by (X, R) → X and f → f . -The writer monad W s X = X ×{tt, ff} * on Set with the monoid of bit strings.

-The strong 2 * -graded lifting of W s along e : ERel → Set, given bẏ

The derived GHL structure is suitable for the semantics of GHL in Example 3.

To complete the structure of the logic, we need to interpret two commands cfTT, cfFF ∈ CExp and set the axioms of commands C c . 

Note, the graded liftingẆ s σ relates only the pair of (x, σ ) and (y, σ ) with common strings of control flow. Hence, the derivation of proof tree of this logic forces the target program to have the same control flow under the precondition.

Example 9 (GHL Structure from the product comonad). In the category Set, the functor CX X × N forms a coproduct-preserving comonad called the product comonad. The right adjoint I : Set → Set C of the coKleisli resolution of C yields a Freyd category with countable coproducts. We next introduce a (N, ≤, 0 max)graded liftingĊ of the comonad C along the fibration p Set : Pred → Set. It is defined byĊn(X, P ) (CX, {(x, m) ∈ X × N | x ∈ P, m ≥ n}). Similarly, we give an (N, ≤, 0 max)-graded Freyd category (J, ) induced by the graded liftinġ C. In this way we obtain a GHL structure.

By instantiating GHL with the above GHL structure, we obtain a program logic useful for reasoning about security levels. For example, when program P 1 requires security level 3 and P 2 requires security level 7, the sequential composition P 1 ; P 2 requires the higher security level 7 (= max (3, 7) ).

We give a simple structure for verifying security levels determined by memory access. Fix a function VarLV : dom(Γ M ) → N assigning security levels to variables. For any expression e, we define its required security level SecLV(e) = sup{VarLV(x) | x ∈ FV(e)}. Using this, for each expression e of sort s ∈ S we introduce a procedure secr e ∈ PExp s called secured expression. It returns the value of e if the level is high enough, otherwise it returns a meaningless contant: The pomonoid (N, ≤, 0, max) in the above can also be replaced with a join semilattice with a least element (Q, ≤, ⊥, ∨). Thus, GHL can be instantiated to a graded comonadic model of security and its associated reasoning.

Several works have studied abstract semantics of Hoare Logic. Martin et al. [31] give a categorical framework based on traced symmetric monoidal closed categories. They also show that their framework can handle extensions such as separation logic. However their framework does not directly model effects and it cannot accommodate grading as is. Goncharov and Shröder [18] study a Hoare Logic to reason in a generic way about programs with side effects. Their logic and underlying semantics is based on an order-enriched monad and they show a relative completeness result. Similarly, Hasuo [20] studies an abstract weakest precondition semantics based on order-enriched monad. A similar categorical model has also been used by Jacobs [23] to study the Dijkstra monad and the Hoare monad. In the logic by Goncharov and Shröder [18] effects are encapsulated in monadic types, while the weakest precondition semantics by Hasuo [20] and the semantics by Jacobs [23] have no underlying calculus. Moreover, none of them is graded. Maillard et al. [29] study a semantics framework based on the Dijkstra monad for program verification. Their framework enables reasoning about different side effects and it separates specification from computation. Their Dijkstra monad has a flavor of grading but the structure they use is more complex than a pomonoid. Maillard et al. [30] focus on relational program logics for effectful computations. They show how these logics can be derived in a relational dependent type theory, but their logics are not graded. As we discussed in the introduction, several works have used grading structures similar to the one we study in this paper, although often with different names. Katsumata studied monads graded by a pomonoid as a semantic model for effects system [24] . A similar approach has also been studied elsewhere [36, 42] . Formal categorical properties of graded monads are pursued by Fujii et al. [13] . Zhang defines a notion of graded category, but it differs to ours, and is instead closer to a definition of a graded monad [55] . As we showed in Section 4, graded categories can be constructed both by monads and comonads graded by a pomonoid, and it can also capture graded structures that do not arise from either of them. Milius et al. [33] also studied monads graded by a pomonoid in the context of trace semantics where the grading represents a notion of depth corresponding to trace length. Exploring whether there is a generalization of our work to traces is an interesting future work.

Various works study comonads graded with a semiring structure as a semantic model of contextual computations captured by means of type systems [7, 16, 44] . In contrast, our graded comonads are graded by a pomonoid. The additive structure of the semiring in those works is needed to merge the gradings of different instances of the same variable. This is natural for the λ-calculus where the context represent multiple inputs, but there is only one conclusion (output). Here instead, we focus on an imperative language. So, we have only one input, the starting memory, and one output, the updated memory. Therefore, it is natural to have just the multiplicative structure of the semiring as a pomonoid. The categorical axiomatics of semiring-graded comonads are studied by Katsumata from the double-category theoretic perspective [25] .

Apart from graded monads, several generalizations of monads has been proposed. Atkey introduces parameterized monads and corresponding parameterized Freyd categories [1] , demonstrating that parameterized monads naturally model effectful computations with preconditions and postconditions. Tate defines productors with composability of effectful computations controlled by a relational 'effector' structure [53] . Orchard et al. define category-graded monads, generalizing graded and parameterised monads via lax functors and sketch a model of Union Bound Logic in this setting (but predicates and graded-predicate interaction are not modelled, as they are here) [41] . Interesting future work is to combine these general models of computational effects with Hoare logic.

We have presented a Graded Hoare Logic as a parameterisable framework for reasoning about programs and their side effects, and studied its categorical semantics. The key guiding idea is that grading can be seen as a refinement of effectful computations. This has brought us naturally to graded categories but to fully internalize this refinement idea we further introduced the new notion of graded Freyd categories. To show the generality of our framework we have shown how different examples are naturally captured by it.

We conclude with some reflections on possible future work.

Future work Carbonneaux et al. present a quantitative verification approach for amortized cost analysis via a Hoare logic augmented with multivariate quantities associated to program variables [8] . Judgments {Γ ; Q}S{Γ ; Q } have pre-and post-conditions Γ and Γ and potential functions Q and Q . Their approach can be mapped to GHL with a grading monoid representing how the potential functions change. However, the multivariate nature of the analysis requires a more fine-grained connection between the structure of the memory and the structure of grades, which have not been developed yet. We leave this for future work. GHL allows us to capture the dependencies between assertions and grading that graded program logics usually use. However, some graded systems (e.g. [4] ) use more explicit dependencies by allowing grade variables-which are also used for grading polymorphism. We plan to explore this direction in future work.

The setting of graded categories in this work subsumes both graded monads and graded comonads and allows flexibility in the model. However, most of our examples in Section 5.3 are related to graded monads. The literature contains various graded comonad models of data-flow properties: like liveness analysis [44] , sensitivities [7] , timing and scheduling [16] , and information-flow control [40] . Future work is to investigate how these structures could be adopted to GHL for reasoning about programs.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Parameterised notions of computation

Proving differential privacy via probabilistic couplings

An introduction to relational program verification

Higherorder approximate relational refinement types for mechanism design and differential privacy

A Program Logic for Union Bounds

Probabilistic relational reasoning for differential privacy

A core quantitative coeffect calculus

Compositional certified resource bounds

Categories for types

Construction of Biclosed Categories

Controlling Effects

Assigning meanings to programs

Towards a formal theory of graded monads

Graded Hoare Logic and its Categorical Semantics. CoRR abs

Combining effects and coeffects via grading

Bounded linear types in a resource semiring

A List of Successes That Can Change the World -Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday

A Relatively Complete Generic Hoare Logic for Order-Enriched Effects

Logical relations for monadic types

Generic weakest precondition semantics from monads enriched with order

coalgebraic Methods in Computer Science

Data-Flow Analyses as Effects and Graded Monads

Categorical Logic and Type Theory

Dijkstra and Hoare monads in monadic computation

Parametric effect monads and semantics of effect systems

A Double Category Theoretic Analysis of Graded Linear Exponential Comonads

Codensity lifting of monads and its dual

Graded Algebraic Theories

Locally graded categories

Dijkstra monads for all

The next 700 relational program logics

Hoare Logic in the Abstract

Functors are Type Refinement Systems

Generic Trace Semantics and Graded Monads

Notions of computation and monads

The program counter security model: Automatic detection and removal of control-flow side channel attacks

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

Semantics with applications

Approximate Relational Reasoning for Probabilistic Programs

Quantitative program reasoning with graded modal types

Unifying graded and parameterised monads

The semantic marriage of monads and effects

Coeffects: Unified static analysis of context-dependence

Coeffects: a calculus of contextdependent computation

Categorical logic

Generic models for computational effects

Environments, continuation semantics and indexed categories

Approximate Relational Hoare Logic for Continuous Random Samplings

Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy

Graded monads and rings of polynomials

Freyd categories are Enriched Lawvere Theories

proceedings of the Workshop on Algebra, Coalgebra and Topology

Programming Languages and Systems -26th European Symposium on Programming

The sequential semantics of producer effect systems

V-indexed categories

Twisted graded algebras and equivalences of graded categories