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 dLtP, 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.