We introduce judgemental theories and their calculi to frame type theory and proof theory in the same mathematical framework. Our analysis sheds light on both the topics, providing a new point of view. In the case of type theory, we provide an abstract definition of type constructor featuring the usual formation, introduction, elimination and computation rules. In proof theory we offer a deep analysis of structural rules, demystifying some of their properties, and putting them into context. We finish the paper discussing the internal logic of a topos, a predicative topos, an elementary 2-topos et similia, and show how these can be organized in judgemental theories.

The talk is based on a joint work with Greta Coraglia: https://arxiv.org/abs/2111.09438

In this talk I will describe four approaches to the semantics of linear logic, focusing on the multiplicative fragment of classical linear logic. I will also explain how these are related.

First, I will recall the usual perspective as a category with extra structure to interpret the connectives, namely a *-autonomous category. Then, I will introduce polycategories where the connectives are defined through a universal properties. The equivalence between the two goes back to Cockett and Seely in 1997 although the version that I will present is slightly modified.

The third approach uses bifibred polycategories. There the connectives are interpreted by fibrational properties. This and it being equivalent to the previous perspective is new. Through some examples I will illustrate how it can be used to build more refined models from existing ones. Finally, it has been observed by Shulman that *-autonomous categories correspond to Frobenius pseudomonoid internal to the 2-polycategory of multivariable adjunctions. I will show how it is connected to the fibrational picture by a polycategorical Grothendieck correspondence.

If time permits I will discuss some subtleties concerning the aforementioned 2-polycategory that calls for a weak variant of the notion of 2-polycategory.

Quatre approches équivalentes pour les modèles de LL

Dans cet exposé je vais décrire quatre façons équivalentes d'assigner une sémantique à la logique linéaire, en me focalisant sur le fragment multiplicatif classique.

Tout d'abord, je rappellerai la perspective usuelle qui consiste à doter des catégories de structures supplémentaires pour interpréter les connecteurs, i.e. les catégories *-autonomes. Puis j'introduirai la notion de polycatégorie dans laquelle les connecteurs sont définis au travers de propriétés universelles. L'équivalence des deux notions a été démontrée par Cockett et Seely en 1997, si ce n'est que la version que je présenterai a été légèrement modifiée.

La troisième perspective utilise la notion de polycatégorie bifibrée. Les connecteurs y sont introduit au moyen de propriétés fibrationelles. Cette approche et le fait quelle est équivalente aux précédentes est nouvelle. J'illustrerai au travers d'exemples comment cela permet de définir de nouveaux modèles plus raffinés à partir de modèles existants.

Enfin, il a été observé par Shulman que les catégories *-autonomes correspondent aux pseudomonoïdes de Frobenius internes à la 2-polycatégorie des adjonctions à plusieurs variables. Je montrerai comment cela est liée à la perspective fibrationnelle au travers d'une correspondance de Grothendieck polycatégorielle.

Si le temps le permet, je discuterai plus en détails certaines subtilités à propos de cette 2-polycatégorie qui poussent à définir une version faible de la notion de 2-polycatégorie.

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

The differential calculus uses addition in a crucial way: this appears clearly in the Leibniz Rule. This is why the differential lambda-calculus as well as differential linear logic feature an unrestricted addition operation on terms (or proofs) of the same type. From an operational point of view, this means that these formalisms feature finite non-determinism. So a natural question arises: is non-determinism inherent to any differential extension of the lambda-calculus and linear logic? Based on intuitions coming from probabilistic coherence spaces, we provide a negative answer to this question, introducing a setting of “summable categories” where the notion of summable pairs of morphisms is axiomatized by means of a functor equipped with three natural transformations satisfying a few axioms. Then we define a notion of differentiation in such a summable category equipped with a resource modality (exponential in the sense of linear logic): this differential structure is a distributive law between a monad associated with the summability structure and the resource comonad, satisfying a few additional axioms. I will present various aspects of this theory (which features similarities with tangent categories), concrete instances of the theory as well as the syntax of a differential version of PCF which can be derived from this general categorical setting. In particular I will show that coherence spaces provide a model of this coherent differentiation, in sharp contrast with differential linear logic.

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very promising, this methodology was previously not fully formalised and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalising the lower-level details, which together enable constructing fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalised in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value λ-calculus, as well as in a simple non-deterministic variant.

This is joint work with Ambroise Lafont.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value λ-calculus, as well as in a simple non-deterministic variant.

This is joint work with Ambroise Lafont.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky. Howe (1989) gave a direct proof that it is a congruence. We propose a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. Example instances include standard applicative bisimilarity in call-by-name and call-by-value λ-calculus, as well as in a simple non-deterministic variant.

This is joint work with Ambroise Lafont.

We show that for any quantale Q, a Q-category is skeletal and complete if and only if it is injective with respect to fully faithful Q-functors. This is a special case of known theorems due to Hofmann and Stubbe, but we provide a different proof, using the characterisation of the MacNeille completion of a Q-category as its injective envelope.