Journées LHC 2019

La deuxième édition des journées LHC aura lieu les 16 et 17 octobre à Lyon.

La première journée (mercredi 16 octobre) sera constituée d’exposés contribués par des participants, autour des thèmes du groupe de travail. Elle se déroulera sur le campus de la Doua.
La deuxième journée (jeudi 17 octobre) sera consacrée à des exposés invités, pour une édition spéciale du séminaire Chocola, commune avec le GT Scalp. Elle aura lieu à l’ENS Lyon et sera suivie de la soutenance de thèse d’Aurore Alcolei.

Les orateurs invités le 17 octobre sont :

Danel Ahman (University of Ljubljana) et Eric Finster (Gallinette, INRIA) pour LHC ;
Dan Ghica (University of Birmingham) et Valeria Vignudelli (École Normale Supérieure de Lyon) pour Scalp.

Par ailleurs, le GT Scalp tiendra symétriquement une journée d’exposés sur ses thèmes le vendredi 18 octobre, toujours à l’ENS Lyon.

Inscription

Les inscriptions sont maintenant closes.

Programme

Mercredi 16 octobre

10h00-10h30 : Accueil

10h30-10h55 : Hugo Herbelin, Univalence par définition en théorie des types cubique

10h55-11h20 : Thibaut Benjamin, Une théorie des types pour les catégories monoïdales

11h20-11h35 : Cédric Ho Thanh, Opetopic algebra

11h35-11h50 : Chaitanya Leena Subramaniam, Deux structures de modèles sur les espaces opétopiques modélisant les (∞,1)-catégories et les ∞-opérades planaires

11h50-12h15 : Kenji Maillard, Relative monads for relational reasoning

12h15-14h00 : Déjeuner

14h00-14h25 : Maxime Lucas, Internalizing abstract rewriting

14h25-14h50 : Nohra Hage, Plactic-like monoids and String Data Structures

14h50-15h05 : Uran Meha, Plactic monoids and rewriting

15h05-15h20 : Cameron Calk, Calculating coherence proofs in modal Kleene algebras

15h20-15h35 : Cyrille Chenavier, Systèmes de réécriture topologiques appliqués aux bases standards et aux algèbres syntaxiques

15h35-16h00 : Marie Kerjean, Reflexitivity in topological vector spaces through mixed chiralities

16h00-16h30 : Café

16h30-16h55 : Marc de Visme, Event Structures for Mixed Choice

16h55-17h10 : Paul-André Melliès, Asynchrony in Concurrent Games and the Gray tensor product of 2-categories

17h10-17h35 : Titouan Carette, Diagrammatic Methods in Quantum Computing

17h35-18h00 : Luidnel Maignan, Ideas on Globally Applied Local Transformations

Jeudi 17 octobre

Séminaire Chocola LHC+Scalp

Vendredi 18 octobre

Journée Scalp

Résumés

Thibaut Benjamin: Une théorie des types pour les catégories monoidales

Cameron Calk: Calculating coherence proofs in modal Kleene algebras

The structure of Kleene algebra was introduced in the context of regular languages, and have been applied in abstract rewriting theory. Augmented with a modal action, confluence results in abstract rewriting theory are formulated and proved internally to these algebras. In this talk I will present a formulation of coherence properties of abstract rewriting systems in the structure of Kleene algebra. Coherence properties from rewriting are captured via a notion of higher-dimensional rewrites, notably in a theorem due to Squier. I will present an algebraic formulation of this theorem for abstract rewriting systems in the context of modal Kleene algebras. A notion of 2-dimensional Kleene algebra will be introduced, as well as characterizations of homotopy bases, globularity and acyclicity internal to these structures. (Work in progress with Eric Goubault, Philippe Malbos and Georg Struth)

Titouan Carette: Diagrammatic Methods in Quantum Computing

The usual model of quantum mechanic involves complex matrices which size scales exponentially with the number of qubits. Categorical quantum mechanic and more particularly the ZX-calculus provides compact representation and a complete equational theory for the design and the verification of quantum processes. This talk will review recent improvements in the expressiveness of such methods and describe some ongoing works on applications for quantum simulation and algorithms.

Cyrille Chenavier: Systèmes de réécriture topologiques appliqués aux bases standards et aux algèbres syntaxiques

Nohra Hage: Plactic-like monoids and String Data Structures

Plactic-like monoids such as plactic, Chinese, hypoplactic, and patience sorting monoids can be defined using combinatorial objects constructed by applying left and right insertion algorithms. An insertion algorithm describes a way to compute a particular combinatorial object starting from a word in the free monoid over a totally ordered alphabet, and the plactic-like monoid arises by factoring this free monoid by the congruence relating words that yield to the same combinatorial object. Moreover, these combinatorial objects are shown to satisfy the cross-section property for the considered plactic-like monoids. In this talk, we will show that the cross-section property can be deduced from the commutation of the left and right insertion algorithms using the notion of string data structures. We will also explain how a morphism of string data structures can transfer combinatorial properties from a string data structure to another one. In particular, we will show how to relate the string data structures of skew tableaux, Young tableaux and quasi-ribon tableaux.

Hugo Herbelin: Univalence par définition en théorie des types cubique

Nous présenterons une variante de la théorie des types cubique de Cohen-Coquand-Huber-Mörtberg dans laquelle l’égalité de type est l’équivalence par définition. Nous esquisserons les liens entre cette variante et les traductions par paramétricité itérée. Ceci est un travail en cours, en commun avec Hugo Moeneclaey

Cédric Ho Thanh: Opetopic algebra

In this short, informal talk, I will start by defining opetopes. In a nutshell, they are schemes of pasting schemes of pasting schemes of pasting schemes of… Motivated by examples (such as categories and planar operads), I will introduce opetopic algebras, and explain how they encompass well-known structures, while simultaneously providing a notion of “higher arity algebra”. Then, we will see that this notion stabilizes (i.e. stops providing fundamentally new examples) in a phenomenon called “algebraic l’oeil”.

Marie Kerjean: Reflexitivity in topological vector spaces through mixed chiralities

Chaitanya Leena Subramaniam: Deux structures de modèles sur les espaces opétopiques modélisant les (∞,1)-catégories et les ∞-opérades planaires

Maxime Lucas: Internalizing abstract rewriting

The goal of this talk is to present a general framework for doing rewriting inside an arbitrary category C. In particular for C the category of Sets we recover Newman’s Lemma, while for C the category of k-Vector spaces we recover the Diamond Lemma. A nice feature of this theory is that it relaxes the usual termination hypothesis. In addition, we expect this theory to generalize nicely to higher dimensional rewriting.

Luidnel Maignan: Ideas on Globally Applied Local Transformations

Kenji Maillard: Relative monads for relational reasoning

Relational verification is concerned with the problem of proving specifications relating either two runs of a single program, such as non-interference, or two different programs, for instance simulations or equivalences. Starting with Benton’s Relational Hoare Logic for imperative programs, many varieties of relational program logics have been designed for specific classes of relational properties and effects. Focusing on the setting of monadic computations, we want to design a generic framework for relational program logics. In our quest to understand the federating principles underlying relational reasoning, we explain how basic core properties of relational program logics are suitably captured by relative monads, a generalization of monads that need not to be an endofunctor. Working “over the product”, these relative monads establish a bridge between two computational monads, employed to encapsulate their relational specifications.

Uran Meha: Plactic monoids and rewriting

The Littelmann path model was introduced in a series of papers in the 90s, as a geometric model for the representation theory of symmetrizable Kac-Moody algebras. The path model features two congruences, respectively the plactic congruence and the one obtained via root operators. Through these two congruences, a generalized plactic monoid is defined for each symmetrizable Kac-Moody algebra. In this talk, I discuss the rewriting interpretation of these congruences. In the special case when the algebra is a semisimple Lie algebra, the corresponding plactic monoid will be shown to admit a certain presentation which satisfies the rewriting properties of termination and confluence. Special attention is paid to the type A case, where the corresponding presentation is known to be coherent.

Paul-André Melliès: Asynchrony in Concurrent Games and the Gray tensor product of 2-categories

Léo Stefanesco: Concurrent Separation Logic and Template Games

Marc de Visme: Event Structures for Mixed Choice

Participants (40)

aurore alcolei (lip)
Emmanuel Beffara (I2M, Université d’Aix-Marseille)
Thibaut Benjamin (Ecole Polytechnique)
Flavien Breuvart (LIPN)
Pierre Cagne (Universitetet i Bergen)
Cameron CALK (LIX (UMR 7161))
Titouan Carette (Université de Lorraine, Inria, CNRS, LORIA)
Cyrille Chenavier (Inria)
Alexandre Clément (LORIA)
Pierre-Yves Coursolle (École Polytechnique - LIX - Équipe COSYNUS)
Marc de Visme (ENS Lyon)
Uli Fahrenberg (LIX)
Simon Forest (LIX)
Zeinab Galal (IRIF)
Alexis Ghyselen (ENS Lyon)
Jean Goubault-Larrecq (LSV, ENS Paris-Saclay)
Nohra Hage (Université Saint-Joseph de Beyrouth (ESIB))
Hugo Herbelin (IRIF - Paris Diderot - Inria)
Tom Hirschowitz (Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS)
Cédric Ho Thanh (IRIF)
Guilhem Jaber (Université de Nantes)
Marie Kerjean (Inria)
Yves Lafont (I2M)
Olivier Laurent (CNRS - ENS Lyon)
Chaitanya Leena Subramaniam (IRIF, Université Paris Diderot)
Maxime Lucas (Inria Rennes)
Luidnel MAIGNAN (LACL, Université Paris-Est Créteil)
Kenji Maillard (Ens Ulm & Inria Paris)
Philippe Malbos (Institut Camille Jordan - UCBL)
Uran Meha (Institut Camille Jordan)
Paul-André Melliès (IRIF, CNRS)
Samuel Mimram (École polytechnique)
Hugo Moeneclaey (Université Paris-Diderot)
Alexey Muranov (Université d’Aix-Marseille)
Federico Olimpieri (Aix-Marseille Université)
Christian Retoré (Univ Montpellier)
Thomas Seiller (CNRS)
Antoine Spicher (LACL UPEC)
Léo Stefanesco (IRIF)
Lionel Vaux (I2M, Aix-Marseille)

Organisation

Pour les 17 et 18 octobre, voir les pages de Chocola et de Scalp.

La journée du 16 octobre aura lieu sur le campus de la Doua.

Les exposés se dérouleront en salle Fokko du Cloux, premier étage du bâtiment Braconnier:

(afficher la carte sur OpenStreetMap)

Le repas de midi aura lieu dans le bâtiment Domus :