The sixth edition of the LHC days will take place on Tuesday 4 and Wednesday 5 June 2024 at LS2N in Nantes.

Registration

Please use this form in order to register (submitting talks is not possible anymore). The deadline for registering is 17 May 2024.

Note that, unfortunately, we will not be able to sponsor travel or local expenses.

Location

The conference will take place in the LS2N (2 chemin de la Houssinière 44300 Nantes):

The talks will be given in the amphitheater located in the ground floor (it can be seen from the entrance behind the glass).

Invited speakers

Dimitri Ara: Construction de Grothendieck et ω-catégories de Gray
Thomas Ehrhard: Intégration dans les cônes

Program (still subject to changes)

Tuesday 4 June 2024

10h45 welcome

11h00 Dimitri Ara: Construction de Grothendieck et ω-catégories de Gray (invited talk)

11h45 Thibaut Benjamin: Computation of inverses in weak ω-categories

12h10 lunch

14h00 Alessandro Di Giorgio: Diagrammatic Algebra of First Order Logic

14h25 Elies Harington: Polynomials in homotopy type theory

14h50 Tanguy Massacrier: Single-set cubical categories and their formalisation with a proof assistant

15h15 break

15h45 Colin Riba: Finitely accessible arboreal adjunctions and Hintikka formulae

16h10 Louise Leclerc: Several approaches to opetopes

16h35 Hugo Herbelin: An investigation into how proofs and programs evaluate in an elementary topos

17h00 end of the day / beginning of the night

Wenesday 5 June 2024

9h00 Thomas Ehrhard: Intégration dans les cônes (invited talk)

9h45 Simon Mirwasser: Indexed differential linear logic and Laplace transform

10h10 break

11h15 Kenji Maillard: Glueing Booleans for Greater Extensionality

11h40 Vincent Moreau: A fibrational approach to regular languages of lambda-terms

12h05 Cole Comfort: A phase-space approach to rewriting infinite-dimensional quantum circuits

12h30 lunch

14h00 Hugo Paquet: Element-free probability distributions and random partitions

14h25 Paul-André Melliès: Transition-based template games

14h50 Axel Kerinec: Towards Categorical Structures for Operational Game Semantics

15h15 break

15h45 Tom Hirschowitz: A semantic notion of inference rule for (dependent, quantitative) type theory

16h10 Peter Hines: Some algebraic & number-theoretic interpretations of associahedra

16h35 Nohra Hage: Combinatorics of super tableaux over signed alphabets

17h00 end of the meeting

Abstracts

Dimitri Ara (Université d’Aix-Marseille)
Construction de Grothendieck et ω-catégories de Gray

Le but de cet exposé est de présenter la construction de Grothendieck pour les ω-catégories strictes et d’expliciter ses fonctorialités naturelles dans le langage des ω-catégories de Gray, c’est-à-dire des catégories enrichies dans la catégorie des ω-catégories strictes munie du produit de Gray.

Thibaut Benjamin (University of Cambridge)
Computation of inverses in weak ω-categories

Alessandro Di Giorgio (University College London)
Diagrammatic Algebra of First Order Logic

The interaction of linear and cartesian bicategories gives rise to first-order bicategories that improve Peirce’s calculus of relations in two ways: (1) their axioms provide a proof systems that is both purely equational and complete; (2) the language has the same expressivity of first-order logic. Since the proof system is purely equation and the syntax is diagrammatic proofs are exactly diagrams rewrites. In particular, our framework nicely accomodate Peirce existential graphs.

https://arxiv.org/pdf/2401.07055.pdf

Cole Comfort (Université de Lorraine, CNRS, Inria)
A phase-space approach to rewriting infinite-dimensional quantum circuits [slides]

The ZX-calculus is a family of graphical languages used to reason about linear maps between finite-dimensional Hilbert spaces. However, the ZX-calculus is by no means bound to Hilbert spaces! By tracking the nondeterministic evolution of discrete position and momentum operators, we show that the stabiliser ZX-calculus can be represented in terms of affine Lagrangian relations over finite fields. In other words, we give a phase-space description of the stabiliser ZX-calculus. Unlike the Hilbert space semantics, this generalises naturally to infinite dimensions: by considering a subcategory of affine Lagrangian relations over the complex numbers, we obtain a ZX-calculus for Gaussian quantum circuits with Dirac deltas. This tracks the nondeterministic evolution of multivariate Gaussian probability distributions between continuous-variable position and momentum operators, which is not possible in Hilbert spaces. Complete equational theories are provided for both the finite and infinite dimensional semantics.

This is based on joint work with Titouan Carette and Robert I. Booth:
https://arxiv.org/pdf/2401.07914
https://arxiv.org/pdf/2403.10479

Thomas Ehrhard (Irif)
Intégration dans les cônes [slides]

Les cônes positifs ont été introduits par Selinger en 2004 et on a montré avec Pagani et Tasson qu’ils sont un modèle de la programmation fonctionnelle probabiliste généralisant les espaces cohérents probabilistes aux types de données “continus”, comme la droite réelle. Ce modèle a cependant un important défaut : il n’est pas vrai qu’un morphisme linéaire entre les cônes des mesures finies sur deux espaces mesurables soit toujours induit par un noyau. Plus fondamentalement il ne dispose que d’une forme restreinte d’échantillonnage qui ne permet pas, par exemple, d’interpréter des langages CBV (dans la traduction “boring” de Girard). Je présenterai une notion d’intégration sur les cônes que nous avons introduite avec Guillaume Geoffroy, très similaire à l’intégrale de Pettis, qui permet de résoudre ces deux problèmes. Celles-ci ont d’autres effets intéressants, notamment sur la notion de type de données vus comme coalgèbres de la comonade !_ sur les cônes intégrables.

Nohra Hage (Institut Catholique de Lille)
Combinatorics of super tableaux over signed alphabets [slides]

We are interested on the combinatorial study of super Young tableaux over signed alphabets of any order. We introduce super Robinson–Schensted–Knuth correspondences between signed two-rowed arrays and pairs of super Young tableaux over signed alphabets. Moreover, we introduce the notion of super Schur functions and give combinatorial descriptions of the super Littlewood–Richardson coefficient for expressing a product of two super Schur functions as a linear combination of super Schur functions.

Elies Harington (Ecole Polytechnique)
Polynomials in homotopy type theory [slides]

Polynomials can be defined in any category with pullbacks, and offer a nice setting to talk about inductive types in type theory (where they are also known as containers) and planar (colored) operads, among other things. Polynomials in higher categories allow the introduction of more symmetric structures, such as some quotient types and symmetric operads. In the setting of Homotopy Type Theory, we show that polynomials in Types are morphisms in a Kleisli category on spans of types, and form the non-linear part of a linear-non-linear adjunction that makes polynomials into a (homotopical) model of linear logic. We also compare this result with an analogue construction with profunctors and generalized species of structure.

Hugo Herbelin (Inria - IRIF)
An investigation into how proofs and programs evaluate in an elementary topos

Elementary toposes are known to have the logical strength of Higher Order Logic which itself has the logical strength of System Fω. More precisely, elementary toposes add propositional extensionality, functional extensionality and unique choice to a variant of Fω with product types and subset types.

We propose to investigate elementary toposes from a Curry-Howard perspective, extracting out extensionality by classifying monomorphims rather than subobjects so that the resulting classifier of fibered-presented propositions into indexed-presented propositions defines only a non-extensional impredicative hProp. We’ll then explore where to find β-equality in the topos structure for conjunctions, disjunctions and quantifiers, as well as for sums and dependent products.

Peter Hines (Dept. of Mathematics, University of York, U.K.)
Some algebraic & number-theoretic interpretations of associahedra [slides]

From their origins in algebraic topology, J. Stasheff’s associahedra now occur in multiple seemingly disjoint fields. This talk simply aims to add more connections to an already long list. We describe how associahedra have interesting connections to some well-established number theory, group theory, and inverse semigroup theory, and make the case that such connections are deeply categorical.

Our starting point is a labelling of the facets of associahedra by P. Erdos’s “exact covering systems” (i.e. pair-wise disjoint sets of modulo classes whose union is the whole of the natural numbers). Based on a connection between some early number-theoretic work of G. Cantor and his later set-theoretic considerations, we demonstrate that distinct facets of associahedra correspond to distinct (ordered) exact covering systems.

Such dissections of a countably infinite set are known to be related to an important class of inverse monoids (Nivat & Perot’s “polycyclic inverse monoids” – also known to linear logicians as “Dynamical Algebras”). We use this connection to label the facets of associahedra by realisations of polycyclic monoids as partial linear injections on the natural numbers.

This allows us to describe maps between distinct facets of the same associahedron in similar terms. Mappings between facets of the same associahedron are elements of Stefan Kohl’s `Class Transposition’ group, and therefore congruential bijections in the sense of J. Conway’s 1972 proof of undecidability in elementary arithmetic. We observe Conway’s motivating example occurring as a mapping between facets of the simplest non-trivial associahedron. A neat relationship between mappings between facets, and embeddings of associahedra into higher-dimensional associahedra, then demonstrates that Conway’s motivating example occurs in all dimensions.

We also consider the special case of the 1-skeleton of associahedra, and identify mappings between facets as giving a realisation of Richard Thompson’s group F. This allows us to express the elements of Thompson’s group in terms of the simple arithmetic problems that motivated Conway.

Finally, we give an entirely categorical interpretation. The congruential bijections that map between facets of a given associahedron are components of natural isomorphisms between functors. The functors in question are unbiased analogues of monoidal tensors (i.e. the setting with one “tensor” of each arity), with the binary case being familiar from linear logic. The above algebraic uniqueness results allow us to give to give a posetal functor groupoid that is an unbiased version of MacLane’s posetal monoidal groupoid W, from the original proof of his coherence theorem for associativity.

We thus identify the algebraic and number-theoretic aspects of associahedra as forms of categorical coherence.

Tom Hirschowitz (LAMA, CNRS, Univ. Savoie Mont Blanc)
A semantic notion of inference rule for (dependent, quantitative) type theory [slides]

Type theory is a family of formal systems ranging from programming language semantics to the foundations of mathematics. In practice, type theories are defined by means of “inference rules”. Everyone in the community understands them to some extent, but they do not have any commonly accepted rigorous interpretation. Or, rather, they have several interpretations, none of which is entirely satisfactory.

In this work, after a brief overview of the literature, we introduce a rigorous, semantic notion of inference rule, our thesis being that most syntactic inference rules written in practice may be directly interpreted in this framework. If time permits, we will sketch how this covers quantitative type theories.

This is joint work in progress with André Hirschowitz and Ambroise Lafont.

Axel Kerinec (INRIA)
Towards Categorical Structures for Operational Game Semantics [slides]

Operational game semantics interprets λ-terms as labelled transition systems (LTS), representing interactions with the environment. The design of the transitions of this LTS is based on the analysis of normal forms of λ-terms. Compared to standard denotational game semantics composition is not a primitive notion. But it is needed in order to obtain categorical structures on such models and have a formal connection with traditional denotational game semantics.

In this talk we will present this categorical composition as well as the challenges encountered to define it.

Louise Leclerc (ENS - PSL)
Several approaches to opetopes [slides]

We will explore different formalizations for the notion of opetope and their relationships. The first, due to Zawadowski, is in terms of face poset [1]. The second, in terms of Zoom Complexes, is due to Koch, Joyal, Batanin and Mascari [2]. Two other formalisms, more recently studied by Pierre-Louis Curien and the speaker, will also be presented.

[1] On positive opetopes, positive opetopic cardinals and positive opetopic set
[2] Polynomial functors and opetopes

Kenji Maillard (Inria)
Glueing Booleans for Greater Extensionality [slides]

Categorical proof of normalisation-by-evaluation (NbE) for the simply typed λ-calculus with extensional sums utilize sheaves over a category of renamings to show the existence of a normal form. Aiming for a similar result applying to a dependent type theory with extensional booleans, this presentation will revisit the construction of the site of renamings and present a synthetic construction of the first steps towards a normalization procedure inside a proof assistant.

Tanguy Massacrier (Université Claude Bernanrd Lyon 1)
Single-set cubical categories and their formalisation with a proof assistant [slides]

We introduce a single-set axiomatisation of cubical ω-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical ω-categories, and their variants with connections and inverses, and the corresponding cubical ω-categories. We also report on the formalisation of cubical ω-categories with the Isabelle/HOL proof assistant, which has been instrumental in finding the single-set axioms.

https://arxiv.org/abs/2401.10553

Paul-André Melliès (IRIF)
Transition-based template games

Simon Mirwasser (LIPN)
Indexed differential linear logic and Laplace transform [slides]

Differential linear logic (DiLL) is an extension of linear logic where one can interpret the differential of a function. Our aim is to refine this logic, in order to interpret linear partial differential equations, with their solutions and their parameters. To do so, we work in a graded setting: the exponential connectives are indexed by elements of an algebraic structure. In recent works, Kerjean and Lemay have shown that the Laplace transform has a crucial role in the denotational semantics of DiLL. Here, we express how this transformation changes the indexes of the exponential connectives, and thus acts on the differential operators. This gives us a framework, graded by two semirings, where we hope to be able to interpret the promotion rule. This is joint work with Marie Kerjean and Yoann Dabrowski.

Vincent Moreau (IRIF, Université Paris Cité, Inria Paris)
A fibrational approach to regular languages of lambda-terms [slides]

Regular languages of lambda-terms have been introduced by Salvati using denotational semantics. They extend the usual regular languages of words and trees to the higher-order setting and permit to use the compositional aspects of the lambda-calculus. In this talk, we revisit the notion of regular languages and present a fibrational setting that permits to establish in a slick and principled way some of their properties. This sheds new light on the fact that regular languages are stable by pullback but not by pushforward.

This is joint work with Paul-André Melliès.

Hugo Paquet (LIPN)
Element-free probability distributions and random partitions [slides]

An “element-free” probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, when elements are used as labels and their specific identity is not important. I will discuss the foundations of element-free distributions in terms of multisets and category theory. In particular I will explain the two main operations for moving between element-free distributions and ordinary distributions. I will then explain how we can use this theory to give a new categorical proof of Kingman’s theorem, a well-known representation theorem for infinite random partitions. (This is joint work with Victor Blanchi.)

Colin Riba (LIP – ENS de Lyon)
Finitely accessible arboreal adjunctions and Hintikka formulae [slides]

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In the examples, equivalence of structures in various fragments of infinitary first-order logic can be captured by transferring bisimilarity along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions finitely accessible. Drawing on this insight, we identify the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka. Thus, the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach relies on Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges’ word-constructions.

Joint work with Luca Reggio.

https://arxiv.org/abs/2304.12709

Participants

Anne Baanen (Vrije Universiteit Amsterdam)
Yoann Barszezak (Université de Savoie)
Thibaut Benjamin (University of Cambridge)
Victor Blanchi (ENS student)
Filippo Bonchi (University of Pisa)
Manuel Catz (IRIF)
Baptiste Chanus (LIPN)
Vikraman Choudhury (Università di Bologna)
Cole Comfort (Université de Lorraine, CNRS, Inria)
Sidney Congard (INRIA - Gallinette)
Raphaëlle Crubillé (Aix-Marseille Université)
Alessandro Di Giorgio (University College London )
Ara Dimitri (Université d’Aix-Marseille)
Thomas Ehrhard (IRIF)
Vincent Franjou (LMJL - Nantes Université)
Pierre Giraud (ex- PhD student at Galinette (Nantes))
Nohra Hage (Institut Catholique de Lille)
Elies Harington (Ecole Polytechnique)
Hugo Herbelin (Inria - IRIF)
Peter Hines (Dept. of Mathematics, University of York, U.K.)
Tom Hirschowitz (LAMA, CNRS, Univ. Savoie Mont Blanc)
Guilhem Jaber (Nantes Université)
Moana Jubert (Inria, IRIF, CNRS, Université Paris-Cité)
Axel Kerinec (INRIA )
Marie Kerjean (CNRS, LIPN)
Yves Lafont (I2M (Institut de Mathématiques de Marseille) AMU (Université d’Aix-Marseille))
Ambroise Lafont (Ecole Polytechnique)
Thomas Lamiaux (Gallinette Team)
Louise Leclerc (ENS - PSL)
Jérémy Ledent (IRIF, Université Paris Cité)
Meven Lennon-Bertrand (University of Cambridge)
Johan Leray (Université de Nantes)
Thea Li (LMF, Université Paris-Saclay)
Noah (Gaïa) Loutchmia ()
Valentin Maestracci (AMU)
Assia Mahboubi (Inria)
Kenji Maillard (Inria)
Georges Maltsiniotis (CNRS-UPC)
Tanguy Massacrier (Université Claude Bernanrd Lyon 1)
Paul-André Melliès (IRIF)
François Métayer (IRIF)
Samuel Mimram (École polytechnique)
Simon Mirwasser (LIPN)
Vincent Moreau (IRIF, Université Paris Cité, Inria Paris)
Guillaume Munch-Maccagnoni (INRIA)
Hugo Paquet (LIPN)
Ada Picano-Nacci (LACL)
Laurent Piriou (Nantes Université (LMJL))
Josselin Poiret (Nantes Université/INRIA)
Colin Riba (LIP – ENS de Lyon)
Amelie Rima (LIP-PLUME)
Alexis Saurin (IRIF)
Nicolas Tabareau (Inria)
Yee-Jian Tan (École Polytechnique)
Sam van Gool (IRIF, Université Paris Cité)
Lionel Vaux Auclair (I2M, Aix-Marseille)

Contacts

In case of any question you can contact the organizers Assia Mahboubi and Nicolas Tabareau (local organizers), Samuel Mimram and Lionel Vaux (LHC coordinators).

LHC days 2024