Journées LHC 2020/2021

In recent works by Amar Hadzihasanovic, a combinatorial presentation of pasting diagrams for higher categorical cells was developed. These objects, called globular posets, are used to describe a certain class of polygraphs as pre-sheaves. Using this point of view, we define a functor realising these combinatorial presentations of higher categories as directed spaces. Furthermore, the directed spaces we obtain are equipped with a cellular decomposition, providing a geometric interpretation of generators and giving rise to a notion of directed CW complex. This is a work in progress.

Uli Fahrenberg: Languages of Higher-Dimensional Automata via Pomset Objects

Motivated by finding proper ways to think about languages of HDA, we introduce a new presentation of precubical sets. Much like simplicial sets are presheaves over totally ordered sets, our “Ziemiański” base category for precubical sets is formed of totally ordered sets with some specially crafted morphisms.

We find this new view on precubical sets susprisingly powerful and use it to introduce precubical sets generated by arbitrary posets, which simplifies and clarifies the role of tracks to define languages of HDA.

Hugo Herbelin: Iterated parametricity and semi-cubical sets: interpreting the universe

Under the equivalence given by Grothendieck’s construction, presheaves over a directed category can be rethought as a fibered-style definition to which an alternative indexed-style definition can be associated. For instance, the indexed presentation of a presheaf on the semi-cube category is a family:

A₀ : U
A₁ : A₀ → A₀ → U
A₂ : Πa₀₀.Πa₀₁.A₁ a₀₀ a₀₁ → Πa₁₀.Πa₁₁. A₁ a₁₀ a₁₁ → A₁ a₀₀ a₁₀ → A₁ a₀₁ a₁₁ → U
⋮

which happens to be at the heart of iterated parametricity. We will give hints on how to define such an indexed definition of semi-cubical sets, i.e. equivalently, on how to effectively define iterated parametricity. We will then give hints about how to interpret a Martin-Löf’s universe as a cubical set in this setting.

Tom Hirschowitz: A categorical framework for congruence of applicative bisimilarity in higher-order languages

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky in 1990. Howe (1989) gave a direct proof that it is a congruence. In previous work with Borthelle (2020), we abstract over this result by proposing a categorical framework for specifying operational semantics, in which we prove that (an abstract analogue of) applicative bisimilarity is automatically a congruence. However, the framework presents a few infelicities:

it requires a non-trivial refinement of the standard approach of Fiore, Plotkin, and Turi (1999) based on monoid algebras for specifying syntax with variable binding;
it relies on so-called prebisimulations instead of the more standard notion of bisimulation by lifting;
one of the axioms, called weak compositionality, feels ad hoc;
the proofs involve directed unions of relations leading to quite a few painful inductions.

In this work, we rectify all of these deficiencies. (Joint work with Ambroise Lafont.)

Meven Lennon-Bertrand: Un calcul des constructions graduel

Le typage graduel est une approche visant à mélanger, dans le même système, des disciplines de typage statiques et dynamiques. L’adaptation de cette méthodologie au calcul des constructions inductives (CIC) pose un certain nombre de problèmes spécifiques, liés à l’absence de séparation types/termes, à l’interdépendance entre typage et calcul, à l’interaction entre erreurs et dépendance… Dans cet exposé, nous présentons une solution à ces problèmes. En utilisant les modèles ordonnés de CIC, on commence par étendre CIC avec une forme de vérification dynamique des types. On construit ensuite un système graduel à types dépendants basé sur cette extension. Le point crucial est de montrer l’équivalent syntaxique, pour la réduction, de propriétés sémantiques des modèles. Cet exposé accompagne la présentation de Kenji Maillard sur les modèles ordonnés de CIC.

Luidnel Maignan: Cellular Automata: examples of Left and Right Kan Extensions

Paraphrasing the famous book of Saunders Mac Lane: “Everything is a Kan Extension”. However, depending on ones background of course, there might not be many examples that arise directly as Kan Extensions. In this talk, we show how the latter describe very naturally local to global definitions, as is the case for cellular automata for instance. Indeed the formal definition simply says “you have a local transformation and a way to compare arbitrary transformations? So simply choose the best global transformation possible!”. This is based on my works with Antoine Spicher and Alexandre Fernandez on so called “Global Transformations”.

Kenji Maillard: Mettons de l’ordre dans CIC!

Le Calcul des Constructions Inductives (CIC) est à la fois un langage de programmation riche et une logique expressive grâce aux types dépendants. Cette richesse complique toutefois l’élaboration d’extensions de CIC. Nous étudions une classe de modèles de CIC où les types sont équipés d’une relation d’ordre. En insistant sur leur caractère effectif, ces modèles peuvent guider la conception de Théories des Types internalisant des structures largement étudiées d’un point de vue purement sémantique. Nous présentons en particulier un modèle inspirés des travaux de Scott fournissant un pendant sémantique à une Théorie des Types graduelle. Cet exposé accompagne la présentation de Meven Lennon-Bertrand sur le Calcul des Constructions Graduel.

Pierre Pradic: Implicit automata in λ-calculi

The talk will be based on joint work with Lê Thành Dũng (Tito) Nguyễn. This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages. After introducing and motivating the problems using Hillebrand and Kanellakis’ result stating that the classes of STLC-definable and regular languages coincide, I will discuss refinements we obtained for linear λ-calculi. I will focus on a correspondence with functions computed by copyless streaming string transducers (SSTs), and particularly on the ingredients of a completeness proof translating λ-terms to transducers. This involves the notions of categorical automata as introduced by Colcombet and Petrisan, categorical models of linear logic and free completions, as well as automata-theoretic techniques related to the composition and determinization of SSTs.

Isaac Ren: Réécriture dans les opérades de battage et résolutions d’opérades

Les opérades de battage (« shuffle operads » en anglais) ont été introduites pour expliciter les actions des groupes symétriques sur les opérades symétriques. Des méthodes de réécriture ont alors été appliquées aux opérades symétriques à travers ces opérades de battage : en particulier, une notion de base de Gröbner a été introduite pour les opérades de battage à partir d’un ordre monomial fixé. Dans cette présentation, nous introduisons la structure de polygraphe de battage comme un cadre général pour la réécriture dans les opérades de battage qui généralise celle des bases de Gröbner en enlevant la contrainte d’ordre monomial pour l’orientation des règles de réécriture. Nous définissons les omega-opérades comme des omega-catégories internes dans la catégorie des opérades de battage, et nous montrons comment étendre un polygraphe de battage convergent en une résolution polygraphique de battage engendré par les chevauchements du polygraphe originel.

Participants

Dimitri Ara
Thibaut Benjamin
Lison Blondeau-Patissier
Cameron Calk
Simon Castellan
Rémy Cerda
Cyrille Chenavier
Jules Chouquet
Pierre-Evariste Dagand
Bérénice Delcroix-Oger
Clovis Eberhart
Uli Fahrenberg
Laura Fontanella
Andrea Gagna
Zeinab Galal
Giulio Guerrieri
Nohra Hage
Michel Hebert
Hugo Herbelin
Tom Hirschowitz
Léo Hubert
Delia Kesner
Meven Lennon-Bertrand
Luidnel MAIGNAN
Kenji Maillard
Philippe Malbos
Samuel Mimram
Alexey Muranov
Lê Thành Dũng Nguyễn
Rémi Nollet
Pierre Pradic
Isaac Ren
Gabriel Scherer
Lutz Strassburger
Aly-Bora Ulusoy
Lionel Vaux Auclair

Contacts

Pour toute question, vous pouvez contacter par mail les organisateurs Samuel Mimram et Lionel Vaux.

Programme

Résumés

Participants

Contacts

Soutiens