# Journées LHC 2018

Les premières *journées LHC* auront lieu sur le campus
Saint-Charles à
Marseille les 17 et 18 octobre 2018. La majeure partie de ces journées sera
constituée d’exposés autour des thèmes du
groupe de travail.

Les inscriptions sont officiellement closes, veuillez prendre directement contact avec les organisateurs si vous souhaitez participer aux journées

## Programme

### Mercredi 17 octobre

**11h-11h30** : Accueil et présentation du GT

**11h30-12h30** (exposé invité) : **Thomas Seiller**, *Dynamics, Algebra and Logic, against Separation*

**12h30-14h00** : Pause repas

**14h00-14h30** : **Andrea Gagna**, *3-foncteurs lax normalisés*

**14h30-15h00** : **Damiano Mazza**, *A Functorial Perspective on Constraint Satisfaction Problems*

**15h00-15h30** : **Paul-André Melliès**, *Template games: a 2-dimensional model of differential linear logic*

**15h30-15h45** : Pause café

**15h45-16h15** : **Zeinab Galal**, *Quotients of λ-terms with Groupoid Actions*

**16h15-16h45** : **Federico Olimpieri**, *On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants*

**16h45-17h15** : **Fabio Pasquali**, *On the formal Church’s Thesis in the Effective topos*

**17h30-18h30** : Business meeting

### Jeudi 18 octobre

**9h-10h** (exposé invité) : **Simon Henry**, *On the Simpson conjecture*

**10h-10h15** : Pause café

**10h15-10h45** : **Cédric Ho Thanh**, *Two syntactical approaches to opetopes*

**10h45-11h15** : **Cameron Calk**, *Time-reversal of homological and homotopical properties in concurrence*

**11h15-11h45** : **Uli Fahrenberg**, *Pomset Languages of Higher-Dimensional Automata*

**11h45-12h15** : **Étienne Miquey**, *A sequent calculus with dependent types for classical arithmetic*

**12h15-13h45** : Pause repas

**13h45-14h15** : **Tom Hirschowitz**, *Monades familiales et sémantique opérationnelle structurelle*

**14h15-14h45** : **Léo Stefanesco**, *An Asynchronous Soundness Theorem for Concurrent Separation Logic*

**14h45-15h15** : **Benjamin Dupont**, *Coherence modulo relations and double groupoids*

**15h15-15h45** : **Cyrille Chenavier**, *Syzygies among reduction operators*

**15h45-16h15** : **Matteo Acclavio**, *From syntactical proof to combinatorial proof*

**16h30** : Clôture

## Résumés

### Orateurs invités

**Simon Henry**, Masaryk University: *On the Simpson conjecture*

In ‘91, Kapranov and Voevodsky erroneously claimed to prove that every weak infinity groupoid (homotopy type) is equivalent to one in which all the composition operations (except inverses) are strict, i.e. a strict infinity category with weak inverse. This is now known to be false, but Carlos Simpson conjectured in 98 that any weak infinity groupoid is equivalent to one were all composition operations are strict, except units and inverses, i.e. a “non-unital strict infinity category” with weak units and weak inverses. He also mentioned that Kapranov and Voevodsky’s paper might contains the proof of this claim. In this talk I will present very recent progress on this conjecture, including a proof of a form of the conjecture in arbitrary dimension, and which indeed use the same ideas as Kapranov and Voevodsky’s original proof. The long term goal is to develop tools to obtain more general strictification theorem, i.e. to understand when certain homotopy structure can be represented by more strict algebraic structures.

**Thomas Seiller**, CNRS et Université Paris 13: *Dynamics, Algebra and Logic, against Separation*

The interplay between logic and computational complexity has been the subject of research for more than 50 years, but it has arguably failed to provide insights on the classification problem. Nevertheless, it has shown how logic is tightly bound to computation, clearly circumscribing the limits of the different approaches. The framework of Interaction Graphs, although taking its roots in logic, offers a mathematical model of programs that bypasses these limits and accounts for subtle aspects of computation. Moreover, it unveils deep connections with methods from geometry and dynamical systems that one may hope to exploit to enable potent proof methods from mathematics to be used by researchers against open problems in complexity theory.

### Exposés des participants

**Matteo Acclavio** (Inria Saclay, LIX): *From syntactical proof to combinatorial proof*

**Cameron Calk** (ICJ): *Time-reversal of homological and homotopical properties in concurrence*

**Cyrille Chenavier** (INRIA Lille): *Syzygies among reduction operators*

Various notions of syzygies exist for describing relations between relations, such as homotopical syzygies, homological syzygies, identities among relations, for instance. In this talk, we define syzygies for linear rewriting systems described by reduction operators. Using lattice operations of reduction operators, we present a procedure for computing the row echelon basis of syzygies. From this procedure, we deduce a lattice criterion for avoiding useless reductions during completion procedures.

**Benjamin Dupont** (ICJ): *Coherence modulo relations and double groupoids*

**Uli Fahrenberg** (LIX): *Pomset Languages of Higher-Dimensional Automata*

We are interested in the language theory of concurrent systems, i.e. systems where there is no total order on events. To model such systems we use the higher-dimensional automata (HDA) of Pratt-van Glabbeek, which have been shown to generalize most other models for concurrent systems which are in use (notably, Petri nets). Executions of such HDA are pomsets, or labeled partial orders; more precisely they are (labeled) interval orders. Languages of HDA are downward-closed (or weak) sets of interval orders, and standard operations on HDA give rise to operations on such languages. One of these is a composition operation which generalizes standard serial composition of pomsets. This is best understood as an ordered pushout in a new category of po(m)sets with interfaces. Joint work with Christian Johansen (Oslo), Georg Struth (Sheffield) and Samuel Mimram (LIX).

**Andrea Gagna** (I2M): *3-foncteurs lax normalisés*

**Zeinab Galal** (IRIF): *Quotients of λ-terms with Groupoid Actions*

**Tom Hirschowitz** (LAMA): *Monades familiales et sémantique opérationnelle structurelle*

We propose an abstract framework for structural operational semantics, in which we prove that under suitable hypotheses bisimilarity is a congruence. We then refine the framework to prove soundness of bisimulation up to context, an efficient method for reducing the size of bisimulation relations. Finally, we demonstrate the flexibility of our approach by reproving known results about congruence of bisimilarity and soundness of bisimulation up to context, in three variants of the π-calculus.

**Cédric Ho Thanh** (IRIF): *Two syntactical approaches to opetopes*

Opetopes are shapes (akin to globules, cubes, simplices, etc.) introduced to describe laws and coherence in higher categories. Their classical definitions, however, makes them difficult to manipulate efficiently. In this presentation, I will sketch the definition of opetopes by Kock et. al., and present ongoing works aiming to describe them completely from a type-theoretic standpoint.

**Damiano Mazza** (CNRS, LIPN, Université Paris 13) : *A Functorial Perspective on Constraint Satisfaction Problems*

**Paul-André Melliès** (IRIF): *Template games: a 2-dimensional model of differential linear logic*

Game semantics is the art of interpreting formulas (types) as games and proofs (programs) as strategies interacting in space and time with their environment. In order to reflect the interactive behaviour of programs, strategies are required to follow specific scheduling policies. Typically, in the case of a purely sequential programming language, the program (Player) and its environment (Opponent) play one after the other, in a strictly alternating way. In the case of a concurrent language, on the other hand, Player and Opponent are allowed to play several moves in a row, in a non alternating way. In the two cases, the scheduling policy is designed very carefully in order to ensure that the strategies synchronise properly and compose well when plugged together. A longstanding conceptual problem has been to understand when and why a given scheduling policy works and is compositional in that sense. In this talk, I will introduce the notion of template game and exhibit a number of simple and fundamental combinatorial properties which ensure that a given scheduling policy defines a monoidal closed bicategory of games, strategies and simulations. The general framework of template game will be illustrated by constructing two game models of (differential) linear logic with different flavours (alternating and non alternating) using the same categorical combinatorics, performed in the category of small categories.

**Étienne Miquey** (INRIA / Université de Nantes): *A sequent calculus with dependent types for classical arithmetic*

In a recent paper, Herbelin developed a calculus dPA^{ω} in which
constructive proofs for the axioms of countable and dependent choices could be
derived via the encoding of a proof of countable universal quantification as a
stream of it components. However, the property of normalization (and therefore
the one of soundness) was only conjectured. The difficulty for the proof of
normalization is due to the simultaneous presence of dependent dependent types
(for the constructive part of the choice), of control operators (for classical
logic), of coinductive objects (to encode functions of type ℕ→A into streams
(a₀,a₁,…)) and of lazy evaluation with sharing (for these coinductive
objects). Building on previous works, we introduce in this paper a variant of
dPA^{ω} presented as a sequent calculus. On the one hand, we take
advantage of a variant of Krivine classical realizability we developed to prove
the normalization of classical call-by-need. On the other hand, we benefit of
dL_{tP}, a classical sequent calculus with dependent types in which type
safety is ensured using delimited continuations together with a syntactic
restriction. By combining the techniques developed in these papers, we manage to
define a realizability interpretation à la Krivine of our calculus that allows
us to prove normalization and soundness.

**Federico Olimpieri** (I2M): *On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants*

**Fabio Pasquali** (Padova): *On the formal Church’s Thesis in the Effective topos*

One of the crucial properties of Hyland’s Effective topos is that its internal logic satisfies the formal Church’s Thesis (CT) [1]. The Effective topos can be obtained by the tripos-to-topos construction, but also in at least two other different ways: as the reg/lex of the category of assemblies or as the ex/lex of the category of partitioned assemblies. Also these two constructions can be described in terms of triposes (or more generally in terms of doctrines [3]). In particular the ex/lex completion is an instance of the construction called elementary quotient completion and introduced in [2].

Since also the category of Assemblies has been proved to be an instance of the elementary quotient completion, in the present talk we use the elementary quotient completion to compare the effective topos and the category of assemblies and we use this approach to prove the validity of (CT) in the internal logic of effective topos.

This is a joint work with M.E. Maietti and G. Rosolini

- J. M. E. Hyland. The effective topos. In A. S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165–216. North-Holland, 1982.
- M. E. Maietti and G. Rosolini. Elementary quotient completion. Theory Appl. Categ., 27:445–463, 2013.
- M. E. Maietti and G. Rosolini. Unifying exact completions. Applied Categorical Structures, 2013

**Léo Stefanesco** (IRIF): *An Asynchronous Soundness Theorem for Concurrent Separation Logic*

Concurrent separation logic (CSL) is a specification logic for concurrent
imperative programs with shared memory and locks. In this paper, we develop a
concurrent and interactive account of the logic inspired by asynchronous game
semantics. To every program C, we associate a pair of asynchronous transition
systems ⟦C⟧_{S} and ⟦C⟧_{L} which describe the operational
behavior of the Code when confronted to its Environment or Frame – both at the
level of machine states (S) and of machine instructions and locks (L). We then
establish that every derivation tree π of a judgment Γ⊢{P}C{Q} defines a winning
and asynchronous strategy ⟦π⟧_{Sep} with respect to both asynchronous
semantics ⟦C⟧_{S} and ⟦C⟧_{L}. From this, we deduce an
asynchronous soundness theorem for CSL, which states that the canonical map
ℒ:⟦C⟧_{S}→⟦C⟧_{L}, from the stateful semantics ⟦C⟧_{S}
to the stateless semantics ⟦C⟧_{L} satisfies a basic fibrational
property. We advocate that this provides a clean and conceptual explanation for
the usual soundness theorem of CSL, including the absence of data races.

## Participants (38)

- Matteo Acclavio (Inria Saclay -LIX)
- Dimitri Ara (Université d’Aix-Marseille)
- Davide Barbarossa (LIPN)
- Emmanuel Beffara (I2M, Université d’Aix-Marseille)
- Thibaut Benjamin (Ecole Polytechnique)
- Cameron Calk (Institut Camille Jordan)
- Cyrille Chenavier (INRIA Lille)
- Jules Chouquet (IRIF, Paris 7)
- Benjamin Dupont (Université Claude Bernard Lyon 1)
- Pasquali Fabio (Università degli Studi di Padova)
- Uli Fahrenberg (LIX, École polytechnique)
- Alexandre Fernandez (LACL, Paris-Est Créteil)
- Simon Forest (Polytechnique)
- Andrea Gagna (Aix-Marseille Université - I2M)
- Zeinab Galal (IRIF)
- Guillaume Geoffroy (AMU)
- Charles Grellois (Aix-Marseille Université)
- Simon Henry (Masaryk University)
- Hugo Herbelin (INRIA - IRIF)
- Tom Hirschowitz (Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS)
- Cédric Ho Thanh (IRIF)
- Yves Lafont (Institut de Mathématiques de Marseille (I2M))
- Chaitanya Leena Subramaniam (Université Paris Diderot (IRIF))
- Luidnel Maignan (LACL, Paris-Est Créteil)
- Kenji Maillard (INRIA Paris)
- Philippe Malbos (Institut Camille Jordan)
- Damiano Mazza (CNRS, LIPN, Université Paris 13)
- Uran Meha (Institut Camlle Jordan)
- Paul-André Mellies (CNRS et Université Paris Diderot)
- Samuel Mimram (École Polytechnique)
- Étienne Miquey (INRIA / Université de Nantes)
- Virgile Mogbil (LIPN, Univ. Paris 13 - CNRS)
- Alexey Muranov (Université d’Aix-Marseille)
- Federico Olimpieri (Aix-Marseille Université)
- Pierre Pradic (LIP, ENS Lyon)
- Thomas Seiller (LIPN)
- Léo Stefanesco (IRIF)
- Lionel Vaux (I2M, université d’Aix-Marseille)

## Organisation

Les journées auront lieu dans la salle de séminaire du 3ème étage de la FRUMAM sur le campus Saint-Charles à Marseille, situé près de la gare :

Afficher une carte plus grande

Les repas de midi sont pris en charge par la rencontre et offerts aux participants.

Attention : l’accès au campus de Saint-Charles est contrôlé. La liste des
participants a été transmise à la loge : signalez que vous venez pour une
rencontre à la FRUMAM pour qu’on vous laisse entrer.
*Une pièce d’identité pourra vous être demandée : merci de penser à en prendre une.*

## Contacts

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