ABSTRACT. The advancement of linear logic has witnessed its core ideas being woven into various forms of type theory, such as System F and dependent type theory. To provide general semantics for these systems, categorical structures have been proposed: linear hyperdoctrines in the case of System F and linear comprehension categories in the case of linear dependent type theory. These notions bear a fundamental similarity in that they are variations on linear-non-linear (LNL) adjunctions. In this work, we make these similarities precise. Specifically, we define a general notion of linear-non-linear adjunction that unifies categorical semantics of different linear type theories. The general notion is a reformulation of the familiar notion internal to 2-categories with finite products. We recover the familiar notion when the ambient 2-category is that of categories, functors and natural transformations. We show that LNL adjunctions are preserved by pseudofunctors that preserve finite products. This gives a method for constructing models of complex linear type theories from simpler models, reducing the workload in individual cases. To substantiate this claim, we show how various concrete models of linear type theories can be obtained via externalization of internal categories.

ABSTRACT. Differential lambda-calculus is an extension of lambda-calculus which enables one to treat differentiation of analytic functions purely syntactically. Just as simply typed lambda-calculus is sound and complete with respect to Cartesian closed categories by the Curry-Howard-Lambek correspondence, simply typed differential lambda-calculus is sound and complete with respect to Cartesian (closed) differential categories. Cockett and Gallagher refined these ideas to provide a categorical semantics of the untyped differential lambda-calculus, introducing the Cartesian differential Turing category with differential canonical codes. This coherently combined a Cartesian differential category with a type of category that provides a sound and complete semantics for the ordinary untyped lambda-calculus: a Turing category with canonical codes. Now, an important source of examples of Cartesian differential categories comes from the categorical semantics of differential linear logic: monoidal differential categories. Briefly, a monoidal differential category is a symmetric monoidal category with a comonad ! and a natural isomorphism d_A : !A \otimes A \to !A, called the deriving transformation, that satisfies certain coherences that capture the fundamental properties of differentiation, like the product rule and chain rule. The coKleisli category of a monoidal differential category is a Cartesian differential category. It is then natural to ask what is the analogue of a monoidal differential category whose coKleisli is a Cartesian differential Turing category. We solve this problem in two stages. First, we define a type of linear category called the linear Turing category (with canonical codes): a linear analogue of the ordinary Turing category (with canonical codes). We show that the coKleisli category of a linear Turing category is an ordinary Turing category. Further, we provide a sufficient condition for its coEilenberg-Moore category to be an ordinary Turing category. Second, we define a monoidal differential Turing category: a linear Turing category with a differential category structure. We show that that this category is the solution to our question. That is, we show that the coKleisli category of a monoidal differential Turing category with additive canonical codes is indeed a Cartesian differential Turing category with differential canonical codes. We also show that this is the unique solution and provide an example of a monoidal differential Turing category: the category of computably enumerable relations.

ABSTRACT. The aim of the present note is to report on ongoing work to investigate the linear fragment of the λ-calculus using the tools of categorical universal algebra, adapting the techniques and ideas developed by Hyland to the linear setting of operads and monoidal categories. We start by investigating algebraic models of the linear λ-calculus through the notion of semiclosed operad and we prove that each of such models gives rise to a linear reflexive object in a closed monoidal category. Inspired by the notion of λ-algebra, we define a category of linear λ-algebras, and we prove that this category is equivalent to that of semiclosed operads. Therefore, combining the two results, we have that every linear λ-algebra gives rise to a linear reflexive object in a closed monoidal category.

ABSTRACT. Multicategories are considered an appropriate setting to model term calculi since they allow a more natural treatment of typing contexts and of the composition rule. Additional structure on them describes structural rules such as the exchange rule, the contraction rule and the weakening rule. Cartesian multicategories with one object are called cartesian operads. This specific class of objects is the setting which we will consider in this talk to categorically describe the untyped lambda calculus seen through the lens of linear logic. In doing so, we refine Hyland's approach to the untyped lambda calculus as a semi-closed algebraic theory. Cartesian operads are equivalent to clones. This equivalence gives us an abstract way to phrase two presentations of the untyped lambda calculus: the more traditional, additive one and the multiplicative one which is in the spirit of linear logic. This result can be extended to the general framework of cartesian Cat-operads and Cat-clones. This then yields two generalizations of the Set-enriched situation where the rewriting theory of the lambda calculus also obtains an explicit algebraic treatment. In this way, the untyped lambda calculus can be both equipped with the structure of a closed Cat-clone and that of a cartesian closed Cat-operad. Moreover, in this richer setting, we obtain by universal construction an equational theory on rewritings that deserves to be further explored. We aim to do so by defining a rewriting theory of the rewritings themselves, bringing together Hyland's and Hilken's approaches.

ABSTRACT. We have recently constructed sequent calculi for non-commutative linear intuitionistic versions of modal logics K, T, K4 and S4 that we have defined via semantics in terms of monoidal categories with a strong monoidal endofunctor, copointed endofunctor, semicomonad or comonad, optionally well-copointed/idempotent. Here we show that the designs of these sequent calculi are directly justified by equivalent semantics of these logics in terms of representable multicategories for suitable notions of (generalized) multicategory and representability: they are presentations of the free such representable multicategories.

ABSTRACT. Assessing quantitative properties of probabilistic programs, like e.g. almost sure termination, is often an undecidable problem. It is, therefore, interesting to identify classes of programs for which these problems become tractable. In a paper to be presented at LICS 2026 (https://arxiv.org/abs/2604.27986) we have shown that the weighted relational model of linear logic can be used to translate (Positive) Almost Sure Termination ((P)AST) for Probabilistic Higher-Order Recursion Schemes (PHORS) into a problem involving generating functions. Then, by using algebraic properties, we have identified a class of PHORS (extending Li et al.’s affine PHORS) whose corresponding generating function is algebraic, making the (P)AST problems decidable. In this abstract, we show that this framework is also fruitful for different quantitative problems and other classes of programs. In particular, we consider two types of quantitative problems: exact inference (i.e. computing the posterior probability distribution generated by a program) and computing the termination probability of a program. To consider inference, we consider Boolean PHORS, a variant of PHORS having a type for the booleans. We then present a typing system that ensures the generating function of a (Boolean) PHORS is either rational or algebraic. In the rational case, we show that exact inference for (Boolean) PHORS is computable and that not only (P)AST is decidable, but the exact value of the probability of termination can be computed in polynomial time. In the algebraic case, we show that we can compute an approximation up to any desired precision of the posterior distribution.

ABSTRACT. We introduce a new exponential modality for coherence spaces that can "count up to 2". Its Kleisli category provides an interesting example of finitary yet intensional semantics of the simply typed λ-calculus. The eventual goal is to present this semantics using an intersection type system, and derive a corresponding notion of graded resource approximants, with a view towards applications to higher-order transducers.

ABSTRACT. By 'enriching' the usual sequent calculus of linear logic over the reals, additives and multiplicatives can be interpreted as addition and multiplication. We thus obtain Quantitative Linear Logic (QLL). Besides the technical curiosity, this creates a bridge between structural methods (chiefly linear logic) and quantitative ones. We support this claim in various ways, and invite the community to further explore this newfound connection. The talk is based on recent work joint with Atkey, Komendantskaya, and Grellois, as well as with Flinkow, Komendantskaya, and Monahan.

ABSTRACT. We present a polymorphic Linear lambda-calculus as a proof language for second-order intuitionistic Linear Logic. The calculus is extended with scalar multiplication and term addition, which enable the proof of a linearity result at the syntactic level. The syntactic linearity yields a correspondence between proof-terms and linear functions. We develop a sound and adequate denotational semantics based on hyperdoctrines valued in semimodule-enriched Linear categories.