La quatrième édition des journées LHC aura lieu les mercredi 12 et jeudi 13 octobre 2022, à l’ENS Paris Saclay, en salle 1Z68.

Pour venir il y a trois options :

1. RER B jusqu’au Guichet puis bus 9 jusqu’au Moulon
2. RER B jusqu’au Guichet puis bus 91.06 jusqu’à l’Université Paris Saclay
3. RER B jusqu’à Massy-Palaiseau puis bus 91.06 jusqu’au Moulon

La première a tendance à être un peu plus rapide. Si vous venez en TGV, vous pouvez prendre un train pour la gare de Massy-Palaiseau pour gagner du temps.

## Programme

Mercredi 12 octobre

13h30-15h: Andrea Gagna

15h30-16h00: Paul-André Melliès

16h00-16h10: pause

16h10-16h40: Louis Lemonnier

16h40-17h10: Vincent Moreau

17h10-17h40: Titouan Carette

Jeudi 13 octobre

9h30-10h00: Giti Omidvar

10h00-10h30: Tom Hirschowitz

10h30-11h: Matteo Acclavio

11h-11h15: pause

11h15-12h45: Valeria Vignudelli

12h45-14h: déjeuner

14h-14h30: Damiano Mazza

14h30-15h00: Yves Lafont

15h00-15h30: Simon Forest

15h30-15h40: pause

15h40-16h10: Éric Goubault

16h10-16h40: Roman Kniazev

## Résumés

Matteo Acclavio: A Graphical Proof System for Logical Clocks

The “happen-before” is an order relation over events playing a special role in formal verification. Some proof theoretical tools are able to handle this relation logically, that is, as a proper connective of the logic. However, the expressiveness of these tools are limited to series-parallel orders.

In this talk I will present proof systems operating on graphs instead of formulas to the aim of overcoming the restrictions coming from the use of in-line formulas. To this aim, the proof theoretical methodologies and notions required to prove analyticity and conservativity in graphical proof systems will be explained.

In particular, I will show a system able to internalize Lamport’s logical clocks algorithm for distributed systems beyond series-parallel orders, proving that the graphical logic it identifies is a conservative extension of a well-known non-commutative logic (on formulas) from the literature.

Titouan Carette: Coends in Categorical Quantum Mechanics

The Categorical Quantum Mechanics program (CQM) aims to understand quantum physics by describing how abstract quantum processes interact with each other. A recent trend in CQM is to redefine quantum process theories via universal properties allowing a purely operational understanding of some categories of super operators. In this context, coends appear as a powerful and surprisingly intuitive tool to construct new process theories. In this talk, I will provide some intuition on coends in this specific setting and sketch the landscape of applications.

El Mehdi Cherradi: Interpreting type theory in a quasicategory: a Yoneda approach

The connection between logics and categories is important and has been studied, notably using a fibrational approach, which has resulted in categorical notions such as that of comprehension categories to connect the syntax of (dependent) type theory and the world of categories. From a semantical point-of-view, there is a well-known correspondence between (the models of) Martin-Löf type theory and locally cartesian closed categories. Motivated by this 1-categorical result, the natural question that arose about the link between (∞, 1)-categories and homotopy type theory has recently found some answers extending the previous logical correspondence to quasicategories, through the simplicial model for homotopy type theory and more generally through (∞, 1)-topoi (the higher version of Grothendieck topoi). Models of (∞, 1)-categories such as quasicategories come with an inbuilt notion of homotopy, which is compatible with all the structure corresponding to some usual structure of 1-categories (for instance limits). However, while this is very convenient to talk about homotopy coherent properties of quasicategories, there happens to be a mismatch with the usual approach to typetheory which involves “strict” features, even when it comes to describing the syntax of homotopy type theory. Our main result consists in providing models of Martin-Löf type theory for a more general class of quasicategories than in the current literature. Most notably, we observe that elementary higher topoi (that is, locally cartesian closed quasicategories with finite limits and colimits, a subobject classifier and enough universes) provide models for homotopy type theory.

https://arxiv.org/abs/2207.01967

Simon Forest: La bicatégorie cartésienne close des spans fins

Dans le modèle Rel de la logique linéaire, les types sont interprétés par des ensembles, et les preuves/programmes par des relations. Une idée naturelle pour avoir un modèle quantitatif, ou proof-relevant (c’est à dire que le modèle garde distinctes les différentes exécutions donnant lieu au même résultat observable), est d’utiliser des spans au lieu de relations. En effet la (bi)catégorie Span, dont les morphismes sont les spans d’ensembles composés par pullback, peut-être vue comme un analogue “proof-relevant”: là où une relation entre A et B ne garde qu’une information binaire (si a et b sont en relation), un span associe à tous a et b un ensemble de témoins, ou de “preuves” qu’ils sont en relation. Malheureusement, une adaptation naïve de l’exponentielle sur Rel ne fonctionne pas sur Span.

D’autres travaux, comme ceux sur les espèces de structure généralisées, fournissent des modèles proof-relevant, mais où la composition nécessite un quotient complexe des témoins, ne présentant ainsi pas l’aspect “concret” du pullback. Bien qu’un quotient semble inévitable, un autre modèle, celui des “jeux concurrents fins”, fait intervenir une composition concrète, sans quotient.

Adaptant les techniques utilisées dans ce dernier modèle, ce travail donne de bons résultats dans la direction d’un modèle de spans de LL, où la composition se fait par des pullbacks classiques. On montre notamment que, pour une pseudocomonade adéquate sur les spans, on obtient une bicatégorie de co-Kleisli cartésienne close.

Ceci est un travail en commun avec Pierre Clairambault.

Andrea Gagna: Fibrations of (∞,2)-categories

In this talk, I will introduce the scaled simplicial sets as a framework for (∞,2)-categories, which are defined by lifting properties that encode in a combinatorial fashion the algebra of 2-categories and the homotopy coherences. Then, I will introduce some fibrations between (∞,2)-categories, which are meant to classify functors from a small (∞,2)-category to the (∞,2)-category of small (∞,2)-categories, in the spirit of the Grothendieck-Lurie correspondence. We give some basic examples of such fibrations, we list a few nice properties and we discuss the semantics of univalence in this framework.

Eric Goubault: Directed homology theories via associative algebras and algebroids / slides

In this talk, we are going to report on directed homology theories, that should provide computable invariants of directed spaces, based on associative algebras, and modules over associative algebras. The aim is twofold. First, we want to recast some of the earlier work involving natural systems (with compositional pairing) in more “classical” algebraic structures, more amenable to direct calculations. Second, we want to make links between these directed homology theories and other approaches, in e.g. non abelian homology (and in particular the semi-abelian approach), and in persistence homology (through the representation theory of quivers and algebras). If time permits, we will hint at a generalization of this work, involving algebroids (“algebras with many objects”) and crossed-modules over algebroids. This is work in progress.

Tom Hirschowitz: A unified treatment of structural definitions on syntax for capture-avoiding substitution, context application, named substitution, partial differentiation, and so on

We introduce a category-theoretic abstraction of a syntax with auxiliary functions, called an admissible monad morphism. Relying on an abstract form of structural recursion, we then design mathematical tools to generate admissible monad morphisms from basic data. These tools automate ubiquitous standard patterns like (1) defining auxiliary functions in successive, potentially dependent layers, and (2) proving properties of auxiliary functions by induction on syntax. We cover significant examples from the literature, including the standard λ-calculus with capture-avoiding substitution, a λ-calculus with binding evaluation contexts, the λ-mu-calculus with named substitution, and the differential λ-calculus with partial differentiation.

This is joint work with Ambroise Lafont.

Roman Kniazev: Chromatic presimplicial model for group knowledge

In this talk, we will present an approach to the semantics of multi-agent epistemic modal logic based on chromatic presimplicial sets. This approach provides an alternative (to Kripke semantics) point of view on knowledge in multi-agent systems. A particular feature of the model is that it can capture non-trivial group knowledge, that is, situations when a knowledge of a group of agents is bigger than a sum of knowledge of agents. We argue that this model highlights an underlying geometric structure of epistemic Kripke frames, which can be further studied with standard topological tools. This is work in progress, joint with Eric Goubault, Jeremy Ledent and Sergio Rajsbaum.

Yves Lafont: Le retour des orientaux

Les orientaux sont une version catégorique supérieure des simplexes introduite par Street en 1987 : dans l’oriental de dimension $n$, chaque cellule est dotée d’une source et d’un but, et non plus de faces comme dans le simplexe correspondant. Une définition inductive élégante obtenue en itérant une monade a été proposée par Burroni en 2000 et un article sommaire publié en 2005, mais la version finale de ce travail remarquable manquait cruellement. Dans notre récent article Orientals as free algebras, nous donnons enfin une description complète de ces orientaux utilisant la théorie des polygraphes, la notion d’expansion, un calcul oriental approprié, et nous montrons qu’ils coïncident avec ceux de Street en appliquant la théorie des complexes dirigés augmentés de Steiner.

C’est un travail commun avec Dimitri Ara et François Métayer : http://arxiv.org/abs/2209.08022.

Louis Lemonnier: Central Submonads and Notions of Computation

The notion of “centre” has been introduced for many algebraic structures in mathematics. A notable example is the centre of a monoid which always determines a commutative submonoid. Monads in category theory are important algebraic structures that may be used to model computational effects in programming languages and in this paper we show how the notion of centre may be extended to strong monads acting on symmetric monoidal categories. We show that the centre of a strong monad $T$, if it exists, determines a commutative submonad $Z$ of $T$, such that the Kleisli category of $Z$ is isomorphic to the premonoidal centre (in the sense of Power and Robinson) of the Kleisli category of $T$. We provide three equivalent conditions which characterise the existence of the centre of $T$ and we show that every strong monad on many well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. We also provide a computational interpretation of our ideas which consists in giving a refinement of Moggi’s monadic metalanguage. The added benefit is that this allows us to immediately establish a large class of contextually equivalent programs for computational effects that are described via monads that admit a non-trivial centre by simply considering the richer syntactic structure provided by the refinement.

Full paper

Damiano Mazza: A Categorical Approach to Descriptive Complexity Theory

Descriptive complexity aims at characterizing complexity classes by reformulating the question “how hard is it for a machine to solve a problem?” to “how hard is it for logic to describe a problem?”. Finite model theory plays a crucial role in the development of this approach to complexity. Categorical logic is a vast generalization of model theory which includes, among many other things, finite model theory. In this talk, we will see how the ideas of descriptive complexity may be used in the context of categorical logic to give interesting characterizations of a number of standard complexity classes.

Paul-André Melliès: A functorial excursion between algebraic geometry and linear logic / slides

The language of Algebraic Geometry combines two complementary and dependent levels of discourse: on the geometric side, schemes define spaces of the same cohesive nature as manifolds ; on the vectorial side, every scheme $X$ comes equipped with a symmetric monoidal category of quasicoherent modules, which may be seen as generalised vector bundles on the scheme $X$. In this presentation, we use the functor of points approach to Algebraic Geometry developed by Grothendieck in the 1970s to establish that every covariant presheaf $X$ on the category of commutative rings — and in particular every scheme $X$ — comes equipped “above it” with a symmetric monoidal closed category $\mathbf{PshMod}_X$ of presheaves of modules. This category $\mathbf{PshMod}_X$ defines moreover a model of intuitionistic linear logic, whose exponential modality is obtained by glueing together in an appropriate way the Sweedler dual construction on ring algebras.

Vincent Moreau: Des mots profinis aux λ-termes profinis

Le but de cet exposé est de combiner les méthodes profinies utilisées en théorie des automates et les modèles du λ-calcul pour obtenir une notion de λ-terme profini. Les mots profinis fournissent un moyen de traiter le comportement spécifique des mots finis par rapport aux automates déterministes. Afin de connecter cette notion de profinitude au λ-calcul, nous considérons le cas des automates d’ordre supérieur qui reconnaissent des λ-termes simplement typés dont les automates de mots et d’arbres sont des cas particuliers.

Notre principale contribution est l’étude de la notion de λ-terme paramétrique au sens de Reynolds. Nous établissons un lien avec les mots profinis dans la double catégorie cartésienne fermée des ensembles finis, fonctions et relations, ce qui correspond aux automates déterministes. Nous prouvons que dans ce cadre, la notion de λ-terme paramétrique coïncide avec la notion classique de mot profini.

Ceci est un travail avec Paul-André Melliès et Sam van Gool.

Giti Omidvar: Combinatorial Flows as Bicolored Atomic Flows

We introduce a new graphical representation of proofs which we call combinatorial flows. They can be seen as a generalization of atomic flows on one side and of combinatorial proofs on the other side. They inherit the close correspondence with open deduction and the possibility of tracing atom occurrences from atomic flows, introduced by Guglielmi and Gundersen. The correctness criterion, on the other hand, is inherited from combinatorial proofs, introduced by Hughes. Hence, combinatorial flows form a proof system in the sense of Cook and Rackhow. In this talk, I will show how to translate an open deduction derivation to a combinatorial flow. Moreover, I will introduce a normalization process called purification for combinatorial flows with units.

Valeria Vignudelli: Equational theories and monads for probabilistic effects

In this talk we will introduce equational theories allowing us to reason on probabilistic computational effects, modeled as monads. For instance, the theory of convex algebras characterizes the monad of probability distributions. Extensions of this theory include the combination of probabilistic and nondeterministic effects, which have led to the development of proof techniques for program equivalence. We will also present recent results on equational theories characterizing monads on metric spaces. These allow us to move from the notion of program equivalence to the notion of program distance.

## Participants

1. Matteo Acclavio
2. Thibaut Benjamin
3. Yoann Barszezak
4. Titouan Carette
5. Rémy Cerda
6. Baptiste Chanus
8. Bryce Clarke
9. Pierre-Louis Curien
10. Aloÿs Dufour
11. Oleon Emile
12. Laura Fontanella
13. Simon Forest
14. Eric Goubault
15. Jean Goubault-Larrecq
16. Elies Harington
17. Tom Hirschowitz
18. Marie Kerjean
19. Roman Kniazev
20. Yves Lafont
22. Louis Lemonnier
23. Muriel Livernet
24. Valentin Maestracci
25. Luidnel Maignan
26. Kenji Maillard
27. Giulio Manzonetto
28. Tanguy Massacrier
29. Damiano Mazza
30. Paul-André Melliès
31. François Métayer
32. Samuel Mimram
33. Simon Mirwasser
34. Vincent Moreau
35. Giti Omidvar
36. Francesca Pratali
38. Colin Riba
39. Morgan Rogers
40. Gabriel Scherer
41. Thomas Seiller
42. Aly-Bor Ulusoy
43. Sam van Gool
44. Lionel Vaux Auclair
45. Renaud Vilmart