A Double Category Theoretic Analysis of Graded Linear Exponential Comonads
Abstract
Graded linear exponential comonads are an extension of linear exponential comonads wih grading, and provide a categorical semantics of resourcesensitive exponential modality in linear logic. In this paper, we propose a concise doublecategory theoretic formulation of graded linear exponential comonads as a kind of monoid homomorphisms from the multiplicative monoids of semirings to the composition monoids of symmetric monoidal endofunctors. We also exploit this formulation to derive the category of graded comonoidcoalgebras, which decompose graded linear exponential comonads into symmetric monoidal adjunctions plus twists.
1 Introduction
One of the important discoveries in substructural logic is the decomposition of the intuitionistic implication \(\phi \Rightarrow \psi \) using the linear implication \(\multimap \) and the exponential modality !. This discovery was studied by Girard through his linear logic, which brought many new ideas and perspectives to logic and programming language semantics.
Inside linear logic proofs, propositions with the exponential modality \(!\phi \) can be freely copied or discarded. Later, it was realized that by adding a copy limit to the exponential modality, like \(!_r\phi \), linear logic gains fine control of assumption usage. This idea was first implemented in bounded linear logic [9], and studied in connection with implicit complexity theory [4, 14]. Indexed exponential modalities \(!_r\) were then used in wider context: resource management in programming languages [3, 7, 8, 20, 23] and control of sensitivity in the metric semantics of programs [5, 21].

We give a new concise formulation of graded linear exponential comonads as vertical monoid homomorphisms from multiplicative monoids of semirings to the composition monoids of symmetric lax monoidal endofunctors. This formulation is given in a rather complex multidouble category of symmetric monoidal categories. The slogan is “to represent a complex structure in a simple category as a simple structure in a complex category”.

In the multidouble category, vertical monoid homomorphisms themselves can be seen as monoids. By considering actions of such monoids, we obtain the concept of graded comonoidcoalgebras. They are an extension of EilenbergMoore coalgebras to graded linear exponential comonads, and the category of graded comonoidcoalgebras provides a resolution of graded linear exponential comonads by a symmetric lax monoidal adjunction plus a twist.
2 Related Work
Graded linear exponential comonads were first introduced as exponential actions in [3], and an equivalent definition was given in [7]. This paper adopts the latter definition as the starting point of study. These papers also consider linear type systems with an indexed exponential modality \(!_r\phi \), which is directly interpreted by a graded linear exponential comonad. This paper, however, focuses only on the categorical axiomatics of the indexed exponential modality, and omit its syntactic theory. In [2], Breuvart and Pagani gave a construction of graded linear exponential comonads from a set of data called stratification. They derived various graded linear exponential comonads on the category of sets and binary relations and the category of coherence spaces. Structures close to, but different from, graded linear exponential comonads were considered in the categorical semantics of the following calculi: INTML for interactive computation [23], coeffect calculus [20] and bounded affine types system [8].
Looking at the dual structure, graded monads, first considered in mathematics [6, 25], were recently used in the semantic study of logic, systems and programming languages [13, 18, 19, 22]. The resolution of graded monads were studied in [12], mildly extending a classic work by Street [26]. The major difference between graded monads and graded linear exponential comonads is the way how they interact with the monoidal structure. In [13] only strengths were considered for graded monads, while graded linear exponential comonads interact with monoidal structures in an intricate manner.
The multicategory of symmetric lax monoidal multifunctors is related to the 2multicategory of Talgebras for a pseudocommutative 2monad T [11]. Hyland and Power studied multifunctors that are symmetric strong monoidal in each argument, while in this paper we weaken “strong” to “lax”. Yet, we think that by suitably extending their theory, the symmetric lax monoidal multifunctors can also be given in the language of 2monad theory.
Monoids in the multicategory \(\mathbf {MSMC}_l\) in Sect. 5 are similar to the distributivity studied in [15], where Laplaza considered two symmetric nonstrict monoidal structures together with a colax distributivity between them. On the other hand, in this paper, we consider a strict monoidal structure on top of the underlying symmetric (nonstrict) monoidal structure, and a lax distributivity between them.
Preliminaries For symmetric monoidal categories and symmetric lax monoidal functors, see [16]. In a symmetric monoidal category \(\mathbb {C}\), by \(\iota :\mathbf {I}\otimes \mathbf {I}\rightarrow \mathbf {I}\) we mean the isomorphism \(\lambda _{\mathbf {I}} = \rho _\mathbf {I}\), and by \(\tau :(A\otimes B)\otimes (C\otimes D)\rightarrow (A\otimes C)\otimes (B\otimes D)\) we mean the symmetry swapping the second and third component of the tensor product. For functors \(F_i:\prod _{j=1}^{m_i}\mathbb {C}_{i,j}\rightarrow \mathbb {D}_i\) where \(1\le i\le n\), we define \(F_1\times \cdots \times F_n\) to be the composite functor \( \textstyle \prod _{1\le i\le n,1\le j\le m_i}\mathbb {C}_{i,j}\rightarrow \prod _{i=1}^n(\prod _{j=1}^{m_i}\mathbb {C}_{i,j})\rightarrow \prod _{i=1}^n\mathbb {D}_i, \) whose codomain is the product category without the nesting of products.
3 Graded Linear Exponential Comonad
In this paper, comonads are graded by a partially ordered semiring. It is a tuple \((R,\le ,0,+,1,*)\) such that \((R,0,+,1,*)\) is a unital semiring (not necessarily commutative) and \(+,*\) are monotone in each argument w.r.t. the partial order \(\le \). The partially ordered monoids of additive and multiplicative parts of R are denoted by \(R^+=(R,\le ,0,+)\) and \(R^*=(R,\le ,1,*)\), respectively.
3.1 Graded Linear Exponential Comonad
Fix a partially ordered semiring \((R,\le ,0,+,1,*)\). We introduce the main subject of this study, Rgraded linear exponential comonad. This concept first appeared in [3, Definition 13] under the name exponential action. We adopt the following definition [7, Sect. 5.2], which is equivalent to the exponential action:
Definition 1

\(D:(R,\le )\rightarrow \mathbf {SMC}_l(\mathbb {C},\mathbb {C})\) is a functor. Below we write \(m_{r}:\mathbf {I}\rightarrow D(r)(\mathbf {I})\) and \(m_{r,A,B}: D (r) (A) \otimes D (r) (B) \rightarrow D (r) (A\otimes B) \) for the symmetric lax monoidal structure of D(r).

\((D,w,c):R^+\rightarrow [\mathbb {C},\mathbb {C}]_l\) is a symmetric colax monoidal functor.

\((D,\epsilon ,\delta ):R^*\rightarrow (\mathbf {SMC}_l(\mathbb {C},\mathbb {C}),\mathrm{Id},\circ )\) is a colax monoidal functor.
They satisfy four equational axioms in Fig. 1. Moreover, we say that D is an Rtwist if Dr is strong monoidal for each \(r\in R\), and \((D,\epsilon ,\delta )\) is a strict monoidal functor (hence \(D1=\mathrm{Id}\) and \(D(r*r')=Dr\circ Dr'\)).
Example 1
Let \(\mathbb {C}\) be a cartesian closed category. We take a partially ordered monoid \(R^\times =(R,\le ,1,\times )\) such that \((R,\le )\) is a join semilattice and \(\times \) preserves joins in both arguments. This condition makes the tuple \(R=(R,\le ,\bot ,\vee ,1,\times )\) a partially ordered semiring. We also take a lax monoidal functor \(G:R^\times \rightarrow \mathbb {C}\). Then the functor \(D:(R,\le )^{op}\rightarrow [\mathbb {C},\mathbb {C}]\) defined by \(DrA=Gr\Rightarrow A\) extends to an \(R^{op}\)graded linear exponential comonad on \(\mathbb {C}\) (here \(R^{op}\) is the orderopposite of R).
Example 2
Continuing the previous example, let \(R=(D,\le ,\bot ,\vee ,\top ,\wedge )\) be a distributive lattice, regarded as a partially ordered semiring. We consider the functor category \([D,\mathbf {Set}]\), where D is regarded as the discrete category of the carrier set D. We then define \(G:R\rightarrow [D,\mathbf {Set}]\) by \((Gr)r'=\emptyset \) if \(r'\not \le r\), and \((Gr)r'=\{*\}\) if \(r'\le r\). This G extends to a lax monoidal functor of type \(G:R^\times \rightarrow [D,\mathbf {Set}]\). From the construction in the previous example, \(DrA=Gr\Rightarrow A\) is a graded linear exponential comonad, which coincides with the masking functor given in [7, Theorem 2]. It behaves as \((DrA)r'=\{*\}\) if \(r'\not \le r\) and \((DrA)r'=Ar'\) if \(r'\le r\). This graded linear exponential comonad is used to model the level of information flow [7, Sect. 6.1].
Example 3
Consider the category \(\mathbf {EPMet}\) of extended pseudometric spaces^{1} and nonexpansive functions between them. It has a symmetric monoidal (closed) structure, whose unit is a terminal object, and whose tensor product is given by \((X,d)\otimes (Y,e)=(X\times Y,d+e)\). It also has the scaling modality \(!_r(X,d)=(X,rd)\), where r is an element of the ordered semiring of nonnegative extended reals, which we denote by \([0,\infty ]\). The scaling modality is a \([0,\infty ]\)twist with respect to the above symmetric monoidal structure.
The concept of Rgraded linear exponential comonad is a generalization of nongraded linear exponential comonad [1, Definition 3]. This was first observed in [3].
Theorem 1
A 1graded linear exponential comonad on a symmetric monoidal category \(\mathbb {C}\) is exactly a nongraded linear exponential comonad on \(\mathbb {C}\).
On the other hand, 1twists make monoidal structures cartesian:
Theorem 2
A 1twist D exists on a symmetric monoidal category \(\mathbb {C}\) if and only if the symmetric monoidal structure of \(\mathbb {C}\) is cartesian (i.e. \(\mathbf {I}\) is terminal and \(\otimes \) is a binary product).
Proof
If it exists, the functor part of D must specify the identity functor \(\mathrm{Id}_\mathbb {C}\) because of the strictness. Next, \((\mathrm{Id},w,c)\) becomes a commutative monoid in \([\mathbb {C},\mathbb {C}]_l\); especially w, c are monoidal natural transformations. From [17, Corollary 17], the monoidal structure of \(\mathbb {C}\) is cartesian. The converse construction is evident.
4 A DoubleCategory Theoretic Reformulation of Graded Linear Exponential Comonad
Although it is in a reasonably compact form, the definition of graded linear exponential comonad is yet technical, and it indeed specifies a quite complex structure. The motivation of this study is to have a conceptually clean and compact definition of it.
However, it is not obvious how to upgrade these axioms to the graded setting, because the concept of “graded coalgebra” and “graded comonoid” are not yet defined, at least for graded linear exponential comonads. Especially, the concept of graded coalgebra should be defined after the concept of graded linear exponential comonad, which we are going to define! From this circularity, the above view of the four axioms are not very helpful when upgrading them in the current situation.
Let us see how 2cell axioms (1) in \(\mathbf {SMC}\) derives the four axioms in Fig. 1.
Proposition 1
5 Multicategory of Symmetric Lax Monoidal Multifunctors
Proposition 1 says that by fixing one index of the doublyindexed natural transformation \(\delta _{,=}:D({}*{=})\rightarrow D{}\circ D{=}\), we obtain a 2cell in the double category \(\mathbf {SMC}\). However, \(\delta \) itself does not live in \(\mathbf {SMC}\). In order to create a room to accommodate \(\delta \) as a kind of 2cell, we extend horizontal morphisms of \(\mathbf {SMC}\) to multiary functors that are symmetric lax monoidal in each argument. We first study such multiary functors in this section.
Let \(\mathbb {C}_i\) (\(1\le i\le n)\) and \(\mathbb {D}\) be symmetric monoidal categories. Intuitively, an nary functor \(F:\mathbb {C}_1\times \cdots \times \mathbb {C}_n\rightarrow \mathbb {D}\) is symmetric lax monoidal in each argument if it comes with a structure making the functor \(F(C_1,..,_m,..,C_n):\mathbb {C}_m\rightarrow \mathbb {D}\) symmetric lax monoidal for each \(m\in \{1,\cdots ,n\}\) and \(C_i\in \mathbb {C}_i\), \(i\in \{1,\cdots ,n\}\backslash \{m\}\). Moreover, these symmetric lax monoidal structures commute with each other in a coherent manner.
To formally define such multiary symmetric lax monoidal functors, we introduce a notation for sequences. For a sequence \(C=C_1,\cdots ,C_n\) of mathematical objects, a natural number \(1\le i\le n\) and another sequence D, by C[i : D] we mean the sequence obtained by replacing \(C_i\) with D. For instance, \((1,3,5)[2:X,Y]=1,X,Y,5\). When D is empty, C[i : ] stands for the sequence obtained by removing the ith element of C.
Definition 2
 1.
For each \(C\in \mathbb {C}_1\times \cdots \times \mathbb {C}_n\) and \(1\le i\le n\), The tuple \((F(C[i:]),\)\(\phi ^i_{C[i:]},\phi ^i_{C[i:,=]})\) is a symmetric lax monoidal functor from \(\mathbb {C}_i\) to \(\mathbb {D}\). We denote it by F(C / i).
 2.
The following equalities hold for each \(C\in \mathbb {C}_1\times \cdots \times \mathbb {C}_n\) and \(1\le i< j\le n\):

\(\phi ^i_{C[j:\mathbf {I}][i:]} = \phi ^j_{C[i:\mathbf {I}][j:]}\)

\(\phi ^j_{C[i:\mathbf {I}][j:P,Q]}\circ (\phi ^i_{C[j:P][i:]}\otimes \phi ^i_{C[j:Q][i:]}) = \phi ^i_{C[j:P\otimes Q][i:]}\circ \iota \)

\(\phi ^i_{C[j:\mathbf {I}][i:P,Q]}\circ (\phi ^j_{C[i:P][j:]}\otimes \phi ^j_{C[i:Q][j:]}) = \phi ^j_{C[i:P\otimes Q][j:]}\circ \iota \)

\(\phi ^j_{C[i:X\otimes Y][j:P,Q]}\circ (\phi ^i_{C[j:P][i:X,Y]}\otimes \phi ^i_{C[j:Q][i:X,Y]})=\phi ^i_{C[j:P\otimes Q][i:X, Y]}\circ (\phi ^j_{C[i:X][j:P,Q]}\otimes \phi ^j_{C[i:Y][j:P,Q]})\circ \tau \).
We note that a symmetric lax monoidal multifunctor of type \(()\rightarrow \mathbb {D}\) is just an object in \(\mathbb {D}\), because all natural transformations vanish and only the functor of type \(1\rightarrow \mathbb {D}\) remains.
Example 4
 1.
For each \(C\in \mathbb {C}\), \((M(,C),\phi ^1_C,\phi ^1_{,=,C})\) and \((M(C,),\phi ^2_C,\phi ^2_{C,,=})\) are symmetric lax monoidal functors of type \(\mathbb {C}\rightarrow \mathbb {C}\).
 2.
The following coherence axioms holds:
 1.
The multiplication \((*)\) is a symmetric lax monoidal multifunctor of type \((R^+,R^+)\rightarrow R^+\).
 2.
The evaluation functor \(ev:[\mathbb {C},\mathbb {C}]_l\times \mathbb {C}\rightarrow \mathbb {C}\) extends to a symmetric lax monoidal multifunctor of type \(([\mathbb {C},\mathbb {C}]_l,\mathbb {C})\rightarrow \mathbb {C}\).
 3.
The functor composition \((\circ )\) extends to a symmetric lax monoidal multifunctor of type \(([\mathbb {C},\mathbb {C}]_l,[\mathbb {C},\mathbb {C}]_l)\rightarrow [\mathbb {C},\mathbb {C}]_l\).
Note that \((*)\) is symmetric strict monoidal in each argument, while \((\circ ), ev\) are symmetric strict monoidal in the first argument, and symmetric lax monoidal in the second argument.
Theorem 3
Symmetric monoidal categories, symmetric lax monoidal multifunctors, and the above multicomposition form a multicategory \(\mathbf {MSMC}_l\).
Proof
(Proof sketch). To check that symmetric lax monoidal multifunctors are closed under multicomposition, the key case is when \(n=2,m_1=m_2=1\) and \(n=1,m_1=2\).
Example 5
(Continued from Example 4). \((R^+,1,*)\) and \(([\mathbb {C},\mathbb {C}]_l,\mathrm{Id},\circ )\) are both lax distributive strict rig categories. Both monoids acts on themselves. The latter monoid acts on \(\mathbb {C}\) with the evaluation functor ev.
6 Graded Linear Exponential Comonads as Vertical Monoid Homomorphisms
We now extend the double category \(\mathbf {SMC}\) of Grandis and Paré by replacing horizontal morphisms with symmetric lax monoidal multifunctors. The concept of 2cells in \(\mathbf {SMC}\) is also replaced by prisms — the reason of the name is because they are placed in the middle of the space surrounded by two horizontal multifunctors and vertical morphisms. Such a prism is defined to be a natural transformation that is a 2cell of \(\mathbf {SMC}\) in each argument.
Definition 3
We note that when \(n=0\), a prism \(\alpha :()\rightarrow W:F\rightarrow G\) is simply a morphism \(\alpha :WF\rightarrow G\) in \(\mathbb {F}\).
Proposition 2
Proposition 3
 1.
\(\beta \circledcirc \alpha \) is a prism of type \((V'_1\circ V_1,\cdots ,V'_n\circ V_n)\rightarrow W'\circ W: F\rightarrow F''\).
 2.
\(\alpha \circledast (\gamma _1,\cdots ,\gamma _n)\) is a prism of type \((U_{1,1},\cdots ,U_{n,m_n})\rightarrow W:F\circ (G_1,\cdots ,G_n)\rightarrow F'\circ (G'_1,\cdots ,G'_n)\).
 3.
The interchange law holds:
Definition 4
Theorem 4
 1.
A vertical monoid homomorphism \((D,\epsilon ,\delta )\) from \((R^+,1,*)\) to \(([\mathbb {C},\mathbb {C}]_l,\mathrm{Id},\circ )\).
 2.
An Rgraded linear exponential comonad on \(\mathbb {C}\).
Vertical monoid homomorphisms vertically compose. Therefore we can extend a graded linear exponential comonad (as a vertical monoid homomorphism) by stacking vertical monoid homomorphisms.
Proposition 4
Let R, S be partially ordered semirings. Then a vertical monoid homomorphism from \((R^+,1_R,*_R)\) to \((S^+,1_S,*_S)\) bijectively corresponds to a monotone function \(h:(R,\le _R)\rightarrow (S,\le _S)\) such that \(h(\sum _R r_i)\le \sum _S h(r_i)\) and \(h(\prod _R r_i)\le \prod _S h(r_i)\) (which we call colax homomorphism).
Proposition 5
Let \(F\dashv U:\mathbb {C}\rightarrow \mathbb {D}\) be a symmetric lax monoidal adjunction. Then the functor \(V^{F\dashv U}\) defined by \(V^{F\dashv U}H=F\circ H\circ U\) is a vertical monoid homomorphism from \(([\mathbb {C},\mathbb {C}]_l,\mathrm{Id},\circ )\) to \(([\mathbb {D},\mathbb {D}]_l,\mathrm{Id},\circ )\).
Proof
Theorem 5
We call the above composite the extension of D with \(F\dashv U\) and h.
7 From Monoid Actions to Graded ComonoidCoalgebras
Definition 5

\((A,u,o):R^+\rightarrow \mathbb {C}\) is a symmetric colax monoidal functor.

\(a_{r,r'}:A(r*r')\rightarrow D (r) (A(r')) \) is a natural transformation.
Proposition 6
When \(R=1\), The category \(C(\mathbb {C},D)\) reduces to the category of EilenbergMoore coalgebras of the nongraded linear exponential comonad.
Theorem 6
Let \((D,w,c,\epsilon ,\delta )\) be a 1graded linear exponential comonad on a symmetric monoidal category \(\mathbb {C}\). Then the category \(C(\mathbb {C},D)\) is strong monoidally isomorphic to the category \(\mathbb {C}^D\) of EilenbergMoore coalgebras of the comonad \((D,\epsilon ,\delta )\).
Theorem 7
Let R be a partially ordered semiring and \((D,w,c,\epsilon ,\delta )\) be an Rgraded linear exponential comonad on a symmetric monoidal category \(\mathbb {C}\).
 1.
The functor \(F:C(\mathbb {C},D)\rightarrow \mathbb {C}\) given by \(F(A,a,u,o)=A1\) and \(Fh=h_1\) is symmetric strict monoidal, and has a symmetric lax monoidal right adjoint \(U:\mathbb {C}\rightarrow C(\mathbb {C},D)\), whose object part is given by \(UA=(\lambda { r}\,.\, DrA, \lambda {r,r'}\, .\, \delta _{r,{r'},A},w_{A}, \)\(\lambda {r,r'}\, .\, c_{r,{r'},A})\).
 2.The following data give an Rtwist T on \(C(\mathbb {C},D)\):Here, \(A=(A,a,u,o)\) and B are Rgraded comonoid coalgebras. From the definition of twists, \(\epsilon ^T,\delta ^T\) are identities.$$\begin{aligned}&TrA=(\lambda {s}~.~A(s*r),~~\lambda {s,s'}~.~a_{s,s'*r},~~u,~~\lambda {s,s'}~.~o_{s*r,s'*r}),\quad (Tr h)_t=h_{t*r}\\&(m^T_r)_t=\mathrm{id}_\mathbf {I},\quad (m^T_{r,A,B})_t=\mathrm{id}_{A(t*r)\otimes B(t*r)},\quad (w^T_{A})_t=u,\quad (c^T_{r,s,A})_t=o_{t*r,t*s}. \end{aligned}$$
 3.
The extension of D with \(F\dashv U\) (Theorem 5) coincides with the Rgraded linear exponential comonad D.
The following classic result [1, Theorem 61] can be reproved by Theorem 7.
Corollary 1
Let \(\mathbb {C}\) be a symmetric monoidal category and Let D be a nongraded linear exponential comonad on \(\mathbb {C}\). The canonical symmetric monoidal structure on the category \(\mathbb {C}^D\) of EilenbergMoore coalgebras of D is cartesian.
Proof
From Theorem 1, D is a 1graded linear exponential comonad on \(\mathbb {C}\). Therefore \(C(\mathbb {C},D)\) has a 1twist by Theorem 73. Therefore the symmetric monoidal structure of \(C(\mathbb {C},D)\) is cartesian by Theorem 2. Finally, \(C(\mathbb {C},D)\) is strong monoidally isomorphic to \(\mathbb {C}^D\) by Theorem 6, hence the symmetric monoidal structure of \(\mathbb {C}^D\) is also cartesian. \(\square \)
Theorem 8
 1.
Equality of symmetric lax monoidal functors \(M\circ K=U\) and \(F\circ M=J\) hold.
 2.
Let \(M^*=\circ M\) and \(M_*=M\circ \) be induced symmetric strict (resp. strong) monoidal functors. Then the following square of symmetric colax monoidal functors commutes.
8 Conclusion
We have given a concise characterization of graded linear exponential comonad as a vertical monoid homomorphism \((D,\epsilon ,\delta )\) from \((R^+,1,*)\) to \(([\mathbb {C},\mathbb {C}]_l,\mathrm{Id},\circ )\). This characterization is built upon a combination of the theory of symmetric lax monoidal multifunctors and Grandis and Paré’s double category of symmetric monoidal categories. After this characterization, we considered monoid actions, and derived the concept of graded comonoidcoalgebras. The category of graded comonoidcoalgebras are shown to give a resolution of the graded linear exponential comonad D. These results are consistent with the theory of nongraded linear exponential comonads developed in [1].
It remains to be seen if the category of graded comonoidcoalgebras can be constructed in a purely doublecategory theoretic way. In nongraded case, there are other type of categorical models of exponential modality using Lafont category and Seely category [17]. Graded version of these categories are also an interesting research topic.
Footnotes
 1.
Here, extended pseudometrics mean the pseudometrics that can return \(+\infty \).
Notes
Acknowledgment
The author is grateful to Marco Gaboardi, Naohiko Hoshino, Flavien Breuvart, Soichiro Fujii and PaulAndrè Melliès for many fruitful discussions. This research was supported by JSPS KAKENHI Grant Number JP15K00014 and ERATO Hasuo Metamathematics for Systems Design Project (No. JPMJER1603), JST.
References
 1.Benton, N., Bierman, G., de Paiva, V., Hyland, M.: Linear \(\lambda \)calculus and categorical models revisited. In: Börger, E., Jäger, G., Kleine Büning, H., Martini, S., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 61–84. Springer, Heidelberg (1993). https://doi.org/10.1007/3540569928_6CrossRefMATHGoogle Scholar
 2.Breuvart, F., Pagani, M.: Modelling coeffects in the relational semantics of linear logic. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, 7–10 September 2015, Berlin, Germany, vol. 41. LIPIcs, pp. 567–581. Schloss Dagstuhl  LeibnizZentrum fuer Informatik (2015)Google Scholar
 3.Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao [24], pp. 351–370CrossRefGoogle Scholar
 4.Dal Lago, U., Schöpp, U.: Functional programming in sublinear space. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 205–225. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642119576_12CrossRefMATHGoogle Scholar
 5.de Amorim, A.A., Gaboardi, M., Hsu, J., Katsumata, S., Cherigui, I.: A semantic account of metric preservation. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 545–556. ACM (2017)Google Scholar
 6.Durov, N.: New approach to Arakelov geometry. arXiv: 0704.2030 v1 [math AG], April 2008
 7.Gaboardi, M., Katsumata, S.Y., Orchard, D.A., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, 18–22 September 2016, pp. 476–489. ACM (2016)Google Scholar
 8.Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao [24], pp. 331–350CrossRefGoogle Scholar
 9.Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomialtime computability. Theoret. Comput. Sci. 97(1), 1–66 (1992)MathSciNetCrossRefGoogle Scholar
 10.Grandis, M., Paré, R.: Adjoint for double categories. Cahiers de Topologie et Gomtrie Diffrentielle Catgoriques 45(3), 193–240 (2004)Google Scholar
 11.Hyland, M., Power, J.: Pseudocommutative monads and pseudoclosed 2categories. J. Pure Appl. Algebra 175(1), 141–185 (2002). Special Volume celebrating the 70th birthday of Professor Max KellyGoogle Scholar
 12.Jacobs, B., Löding, C. (eds.): FoSSaCS 2016. LNCS, vol. 9634. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662496305CrossRefGoogle Scholar
 13.Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 633–646. ACM (2014)Google Scholar
 14.Lago, U.D., Gaboardi, M.: Linear dependent types and relative completeness. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp. 133–142, June 2011Google Scholar
 15.Laplaza, M.L.: Coherence for distributivity. In: Kelly, G.M., Laplaza, M., Lewis, G., Mac Lane, S. (eds.) Coherence in Categories. LNM, vol. 281, pp. 29–65. Springer, Heidelberg (1972). https://doi.org/10.1007/BFb0059555CrossRefGoogle Scholar
 16.Mac Lane, S.: Categories for the Working Mathematician. GTM, vol. 5. Springer, New York (1978). https://doi.org/10.1007/9781475747218CrossRefMATHGoogle Scholar
 17.Melliès, P.A.: Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, vol. 27. Panoramas et synthses. Société Mathématique de France (2009)Google Scholar
 18.Melliès, P.A.: The parametric continuation monad. Math. Struct. Comput. Sci. 27(5), 651–680 (2017)MathSciNetCrossRefGoogle Scholar
 19.Milius, S., Pattinson, D., Schröder, L.: Generic trace semantics and graded monads. In: Moss, L.S., Sobocinski, P. (eds.) 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, 24–26 June 2015, Nijmegen, The Netherlands, vol. 35. LIPIcs, pp. 253–269. Schloss Dagstuhl  LeibnizZentrum fuer Informatik (2015)Google Scholar
 20.Petricek, T., Orchard, D., Mycroft, A.: Coeffects: unified static analysis of contextdependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 385–397. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642392122_35CrossRefGoogle Scholar
 21.Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, 27–29 September 2010, pp. 157–168. ACM (2010)Google Scholar
 22.Sato, T.: Approximate relational Hoare logic for continuous random samplings. Electr. Notes Theor. Comput. Sci. 325, 277–298 (2016)MathSciNetCrossRefGoogle Scholar
 23.Schöpp, U.: Computationbyinteraction with effects. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 305–321. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642253188_23CrossRefGoogle Scholar
 24.Shao, Z. (ed.): ESOP 2014. LNCS, vol. 8410. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642548338CrossRefGoogle Scholar
 25.Smirnov, A.L.: Graded monads and rings of polynomials. J. Math. Sci. 151(3), 3032–3051 (2008)MathSciNetCrossRefGoogle Scholar
 26.Street, R.: Two constructions on lax functors. Cahiers de Topologie et Géométrie Différentielle Catégoriques (1972)Google Scholar
Copyright information
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 book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book'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.