Journées d'hiver 2022-23 du GT Scalp

Du 15 au 17 février 2023 au CIRM (Marseille)

Introduction

Les rencontres d'hiver 2022-23 du GT Scalp se sont déroulées au CIRM à Marseille du 15 février en fin de matinée jusqu'au 17 février en début d'après-midi.

Le programme est disponible ci-dessous; pour la plupart, les supports d'exposés sont également disponibles.

À l'issue des rencontres, une motion a été adoptée au sujet de la réforme des retraites, le texte est disponible ici.

Exposés invités

  • Sylvie Boldo (DR Inria, Inria Saclay): Exposé reporté
  • Marie Kerjean (CR CNRS, LIPN, Université Sorbonne Paris Nord): Exponential functions and exponential connectives: turning the Taylor expansion into a monad
    • Differential Linear Logic (DiLL) adds to Linear Logic a symmetrization of three out of four exponential rules, and by doing so allows the typing of higher-order functional analysis.
      In this talk, I will explore the denotational interpretation of the missing fourth rule, symmetric to the promotion one. We will show that it is necessary interpreted by an exponential map, alike the scalar function e^x. Miraculously, this exponential map enjoys a dynamic, in terms of cut-elimination or coherence diagrams, which is symmetrical to the promotion rule. I will explain why the existence of this new exponential rule implies a monad on the “of course” exponential connective, and enforce the existence of a quantitative setting. I will explore different models of Linear Logic such as Rel which enjoy indeed a copromotion. I will also explain a graded smooth model of this new exponential rule, in which indices witness the exponential growth of higher-order smooth functions. Finally, we give an explanation of the apparent miraculous symmetry of DiLL rules: when it exists, the Laplace transformation changes each co-structural rule of DiLL into the original structural rule of LL. This is joint work with Jean-Simon Lemay.
  • Étienne Miquey (MCF I2M, Aix-Marseille Université): Evidenced Frames: A Unifying Framework Broadening Realizability Models
    • Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. Nonetheless, the existing literature on realizability models has several limitations, including the following:
      1) first of all, the question “What is a realizability model?” does not have a very satisfying formal answer
      2) traditional realizability models have a rather limited notion of computation, which only supports non-termination and avoids many other commonly used effects. Work to address these limitations has typically overlaid structure on top of existing models, such as by using powersets to represent non-determinism, but kept the realizers themselves deterministic.
      3) The algebraic structure of existing realizability models taking into account effects in a more direct fashion (as is done in Krivine realizability for instance) is hard to analyze.
      In this work, we (Liron Cohen, Ross Tate & myself) alternatively address these limitations by introducing evidenced frames: a general-purpose framework for building realizability models that support diverse effectful computations. We demonstrate that they define a very flexible notion of realizability models, allowing in particular models wherein the realizers themselves can be effectful, such as λ-terms that can manipulate state, reduce non-deterministically, or fail entirely. Beyond the broader notions of computation, we demonstrate that evidenced frames form a unifying framework for (realizability) models of higher-order dependent predicate logic. In particular, we prove that evidenced frames are complete with respect to these models, and that the existing completeness construction for implicative algebras—another foundational framework for realizability—factors through our simpler construction. As such, we conclude that evidenced frames offer an ideal domain for unifying and broadening realizability models.
  • Hugo Paquet (University of Oxford, Royaume-Uni): Call-by-value in bicategories of games
    • Game semantics is naturally described using a bicategory, rather than a category, because the composition of strategies is only associative and unital up to isomorphism.
      This situation makes it difficult to relate game semantics to the categorical theories of effects and resources developed by Moggi, Melliès, and many others. In this talk I will describe new notions in bicategory theory: strong pseudomonads and premonoidal bicategories, that can be used for the semantics of call-by-value languages.
      As the main motivating example, I will discuss the bicategorical structure of concurrent games, and the universal properties that we can use to prove the coherence axioms.
      This is based on joint work with Philip Saville.

Inscriptions et propositions d'exposé

Carte postale

Inscription

L'inscription est gratuite mais obligatoire, à effectuer sur:

https://conferences.cirm-math.fr/2992.html

L'inscription comprend les repas (3 déjeuners, 2 dîners) et l'hébergement (2 nuits) au CIRM. Elle est à effectuer avant le

16 janvier 2023

Propositions d'exposé

Les propositions d'exposés se font en deux étapes:

  • a) Lors de l'inscription, vous serez invités à dire si vous souhaitez proposer un exposé.
  • b) Si oui, vous pouvez envoyer vos titres / abstracts à pierre.clairambault@cnrs.fr.
  • Nous ne manquerons pas de vous recontacter pour récupérer les titres / abstracts manquants !

La durée des exposés n'a pas encore été fixée, elle dépendra du nombre de propositions et des souhaits des orateurs/oratrices.

Comme d'habitude, nous apprécions spécialement les contributions des jeunes (doctorant(e)s et post-doc) et demandons aux encadrant(e)s d'encourager leurs encadré(e)s à présenter leurs travaux.

Informations pratiques

Pour l'accès au CIRM, voir https://www.fr-cirm-math.fr/venir-au-cirm.html

Les exposés se tiendront dans l'amphithéatre A2.

Le programme commencera le mercredi 15 après le repas, pour permettre aux participants de voyager le matin. Dans la mesure du possible, nous nous efforcerons de terminer tôt le vendredi après-midi.

Programme

La liste des exposés avec les résumés est disponible ci-dessous.

(Les horaires sont aussi accessibles sur le site du CIRM en suivant ce lien.)

Liste des exposés contribués

  • Davide BARBAROSSA:
    • Lambda-calculus goes to the tropics
    • Among the approaches directed towards the analysis of quantitative properties of programs, one can certainly mention the metric approaches and the differential/resource-aware ones. In both, the notion of (non-)linearity in the sense of linear logic plays a central role: the first ones aim at treating program distances, and duplication leads to interpret bounded programs as Lipschitz maps; the second ones aim at directly handling duplication in the syntax, and duplication leads to interpret programs as power series.
      A natural question is thus whether these two apparently unrelated ways of handling (non-)linearity can be somehow connected. At a first glance, there seems to be a “logarithmic” gap between the two: in metric models n duplications result in a Lipschitz function nx, while in differential models this results in a polynomial x^n, not Lipschitz.
      The central insight of my talk is that a natural way to overcome this obstacle and bridge these two viewpoints is to develop differential semantics in the setting of tropical mathematics, which is a rich and florid combinatorial counterpart of usual algebraic geometry in tight relation with optimization and computational problems.
  • Nicolas BLANCO:
    • The Grothendieck construction as a pullback
    • Indexed sets are families of sets indexed by another set. There are various equivalent ways of defining it. One is to consider that an indexed set is given by a function f : A → B where B is the indexing set. The family of sets is then obtained by considering the fibres of f. For each element b in B one gets a set by considering the preimage of b by f. Alternatively, one can defined an indexed set by assigning to each element of b a set. This can be presented as a functor F : B → Set from B considered as a discrete category into the category of sets and functions. This two point of views can be categorified in order to get a notion of indexed category. An indexed category can be presented as a functor F : C → D with some extra properties, namely a fibration. Alternatively, it can be regarded as a pseudofunctor from D into Cat the bicategory of (small) categories, functors and natural transformations.
      The Grothendieck construction is the process that turns a functor F : B → Set into a function π : ∫F → B, and similarly for the categorified version. The set ∫F has as elements pairs (b,x) of an element b in B and an element x in F(b). One way of understanding the Grothendieck construction is as a pullback. It is the result of pulling the forgetful functor U : Set_pt → Set along F, where Set_pt is the category of pointed sets and functions preserving the point. However, since this pullback is performed in Cat, it only exhibits π : ∫F → B as a functor from a category into the discrete category B. It is still necessary to justify that ∫F is a discrete category. Similarly, in the categorified version, considering the Grothendieck construction as a pullback only says that from any pseudofunctor from D into Cat, one gets a pseudofunctor into D. Some justification is needed to show that this is actually a functor of categories.
      In this talk, I will more generally consider pullbacks in the category of virtual double categories and functors of virtual double categories. I will give sufficient conditions under which these pullbacks form double categories, bicategories, categories or sets. I will then apply it to the previous Grothendieck constructions as well as other variations of the Grothendieck construction.
  • Flavien BREUVART:
    • A fibrational approach to Indexed Linear Logic
  • Simon CASTELLAN:
    • Mathematical Foundations of Plant Semantics
    • What is a plant? What is a species? We will finally answer those long-standing questions using the full power of algebraic types, probablistic logics, bayesian inference, information theory, and quantitative orthogonality.
  • Remy CERDA:
    • Taylor Expansion for the Infinitary λ-Calculus
    • The Taylor expansion is an approximation framework for the λ-calculus that has been fruitfully adapted to several of its variants. Many results arise from a Commutation theorem relating the β-reduction of a term to the dynamics induced on its Taylor approximation, which leads to characterisations of both qualitative (e.g. normalisability) and quantitative properties of the λ-calculi under consideration.
      We extend this framework to an infinitary λ-calculus (where both λ-terms and β-reductions may be infinite). This enables us to provide new, simple proofs of some properties of this calculus, as well as new characterisations of its normalisation properties. In turn, this infinitary λ-calculus turns out to be a reasonable setting for the study of the Taylor approximation of usual, finite λ-terms.
  • Pablo DONATO:
    • Compiling gestural actions with deep inference
    • We present Actema, a prototype of user interface where formal proofs can be built through gestural actions, and its integration within Coq through the coq-actema plugin. In particular, the semantics of drag-and-drop actions rely on subformula linking, a kind of deep inference proof system which builds synthetic inference rules for axiom links. Through a deep embedding of first-order logic in Coq, these actions are then compiled to tactics by computational reflection of the semantics.
  • Giulio GUERRIERI:
    • Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
    • A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.
      This is joint work with Luc Pellissier and Lorenzo Tortora de Falco.
  • Jean-Baptiste JOINET:
    • Dissymetrical Linear Logics
    • This paper is devoted to design computational systems of linear logic (i.e. systems in which, notably, the non linear and structural phenomena which arise during the cut-elimination process are taken in charge by specific modalities, the exponentials: ! and ?). The systems designed are “intermediate” between Intuitionistic LL and Classical LL. Methodologically, the focus is put on how to break the symmetrical interdependency between ! and ? which prevails in Classical LL – and this without to loose the computational properties (closure by cut-elimination, atomizability of axioms). Four main systems are designed (Dissymetrical LL, semi-functorial Dissymetrical LL, semi-specialized Dissymetrical LL, bi-conclusion LL), where, in each of them, ! and ? play well differentiated roles.
  • Kenji MAILLARD:
    • Adding boolean extensionality to intensional dependent type theory
    • Dependently-typed based proof assistant usually implemement variants of intensional type theory for decidability purposes. However, for usability purposes, adopting extensionality principles in the type theory can tremendously reduce the boilerplate that proof assistant users have to input. Following the fine trail to keep a decidable yet powerful equational theory for intensional type theory, I propose a strategy to extend intensional Martin-Lof type theory (with Π,Σ,𝔹 and a universe ◻) with an extensionality principle for booleans.
  • Samuel MIMRAM:
    • Division by 2, in homotopy type theory
    • Natural numbers are isomorphism classes of finite sets and one can look for operations on sets which, after quotienting, allow recovering traditional arithmetic operations. Moreover, from a constructivist perspective, it is interesting to study whether those operations can be performed without resorting to the axiom of choice (the use of classical logic is usually necessary). Following the work of Bernstein, Sierpiński, Doyle and Conway, we study here “division by two” (or, rather, regularity of multiplication by two). We provide here a full formalization of this operation on sets, using the cubical variant of Agda, which is an implementation of the homotopy type theory setting, thus revealing some interesting points in the proof. As a novel contribution, we also show that this construction extends to general types, as opposed to sets. This is joint work with Emile Oleon.
  • Guillaume MUNCH-MACCAGNONI:
    • Programme for a rational reconstruction of ownership in PLs
  • Lê Thành Dũng NGUYEN:
    • A complexity gap between pomset logic and system BV
    • Pomset logic and system BV are two similar extensions of Multiplicative Linear Logic with Mix: they both add a new multiplicative connective which is non-commutative and self-dual. Both require going beyond the limits of the sequent calculus: pomset logic uses proof nets while BV was the first application of deep inference.
      It had been conjectured for two decades that these two logics are equivalent, i.e. prove the same formulas. Lutz Straßburger and I recently found a counterexample: a formula provable in pomset logic but not in BV (conversely, it is known that BV-provable implies pomset-provable). Moreover, we showed that pomset logic is complete for the second level of the polynomial hierarchy, while BV is known to be NP-complete.
  • Federico OLIMPIERI:
    • Coherence by Normalization for Linear Multicategorical Structures
    • We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms who live in the free multicategorical structures are the same whenever the normal forms of the associated class of terms are equal. As an application, we obtain syntactic proofs of Mac Lane's coherence theorems for (symmetric) monoidal categories.
  • Giti OMIDVAR:
    • The Composition of Combinatorial Flows
    • In this talk, I will introduce combinatorial flows, for classical propositional logic, which are a graph representation of proofs. They can also be seen as a generalization of atomic flows and combinatorial proofs. From atomic flows, they inherit the close correspondence with deep inference and the possibility of tracing the occurrences of atoms in a derivation. They inherit the correctness criterion from combinatorial proofs. This allows the reconstruction of the derivation from the flow. In fact, combinatorial flows form a proof system in the sense of Cook and Reckhow. We show how to translate between deep inference derivations and combinatorial flows. Moreover, we present the normalization steps for combinatorial flows. We also talk about the termination of these rewriting steps.
  • Wendlasida OUEDRAOGO:
    • Generating formally verified lexers with Coqlex
    • A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool chain. The Compcert[1] project, a formally verified C compiler, comes with associated tools and proofs that allow one to formally verify most of those components. However, some components, in particular the lexer, remain unverified. To contribute to the end-to-end verification of compilers, we implemented a verified lexer generator whose usage is similar to OCamllex[2]. Our software, called Coqlex [3], reads a lexer specification and generates a lexer equipped with Coq proofs of its correctness. It provides a formally verified implementation of most features that standard lexer generators (that are not formally verified) usually have. We also give a performance evaluation, comparing Coqlex to OCamllex and Verbatim++[4, 5].
      Refs:
      [1] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler.
      [2] Joshua B Smith. 2007. Ocamllex and Ocamlyacc. Practical OCaml
      [3] Wendlasida Ouedraogo, Danko Ilik and Lutz Strassburger. 2021. Coqlex, an approach to generate verified lexers (very first version)
      [4] Derek Egolf, Sam Lasser, and Kathleen Fisher. 2021. Verbatim: A Verified lexer generator.
      [5] Derek Egolf, Sam Lasser, and Kathleen Fisher. 2022. Verbatim++: verified, optimized, and semantically rich lexing with derivatives
  • Luc PELLISSIER:
    • Versioning the law
  • Sam VAN GOOL:
    • Propositional Quantifiers and Uniform Interpolation

Participants

  1. Davide BARBAROSSA, Università di Bologna
  2. Esaïe BAUER, Université Paris Cité
  3. Nicolas BLANCO, University of Birmingham
  4. Vincent R.b. BLAZY, Université de Paris
  5. Lison BLONDEAU-PATISSIER, I2M, Aix-Marseille Université
  6. Valentin BLOT, INRIA, LMF, Université Paris-Saclay
  7. Sylvie BOLDO, Inria et Université Paris-Saclay
  8. Pierre BOUDES, Univ. Paris 13
  9. Flavien BREUVART, Univ. Sorbonne Paris Nord (ex. P13)
  10. Simon CASTELLAN, Inria
  11. Rémy CERDA, Aix-Marseille Université
  12. El Mehdi CHERRADI, IRIF, Université de Paris
  13. Gregory CHICHERY, LIS
  14. Pierre CLAIRAMBAULT, CNRS LIS, Aix-Marseille Université
  15. Sidney CONGARD, Université Paris Cité
  16. Raphaëlle CRUBILLÉ, CNRS Laboratoire d'Informatique et Systèmes
  17. Marc DE VISME, Inria Saclay Ile de France
  18. Raffaele DI DONNA, IRIF
  19. Pablo DONATO, Institut Polytechnique de Paris
  20. Aloÿs DUFOUR, LIPN Université Sorbonne Paris Nord
  21. Hugo FEREE, Université Paris Cité
  22. Simon FOREST, Aix-Marseille Université
  23. Giulio GUERRIERI, Aix-Marseille Université, LIS
  24. Elies HARINGTON, LIX
  25. Hugo HERBELIN, IRIF - Université Paris Cité
  26. Farzad JAFARRAHMANI, Institut de recherche en informatique Paris
  27. Jean-Baptiste JOINET, University Jean Moulin Lyon 3
  28. Moana JUBERT, Université Paris-Cité
  29. Chantal KELLER, LMF, Université Paris-Saclay
  30. Axel KERINEC, Université Sorbonne Paris Nord
  31. Marie KERJEAN, LIPN, CNRS, Université Sorbonne Paris Nord
  32. Vijay Dave KINNARI, LMF, Université Paris-Saclay
  33. Louis LEMONNIER, ENS Paris-Saclay
  34. Kenji MAILLARD, Inria Rennes-Bretagne Atlantique
  35. Fabio MASSAIOLI, Scuola Normale Superiore, Pisa
  36. Damiano MAZZA, CNRS CNRS - Université Sorbonne Paris Nord
  37. Samuel MIMRAM, École polytechnique
  38. Étienne MIQUEY, Aix-Marseille Université
  39. Guillaume MUNCH-MACCAGNONI, INRIA
  40. Le Thanh Dung NGUYEN, École normale supérieure de Lyon
  41. Federico OLIMPIERI, University of Leeds
  42. Faustine OLIVA, Aix-Marseille Université
  43. Giti OMIDVAR, INRIA Saclay & Ecole Polytechnique Paris
  44. Wendlasida OUEDRAOGO, INRIA Saclay
  45. Hugo PAQUET, University of Oxford
  46. Luc PELLISSIER, Université Paris Est Créteil
  47. Loïc PEYROT, IRIF, Université Paris Cité
  48. Laurent REGNIER, Aix-Marseille Université
  49. Morgan ROGERS, LIPN, USPN
  50. Alexis SAURIN, CNRS Laboratoire IRIF, Paris
  51. Will TROIANI, LIPN
  52. Sam VAN GOOL, Université Paris Cité
  53. Lionel VAUX AUCLAIR, Aix-Marseille Université
  54. Jui-Hsuan WU, Institut Polytechnique de Paris & INRIA Saclay

Comité d'organisation

  • Pierre Clairambault
  • Raphaëlle Crubillé
  • Chantal Keller
  • Damiano Mazza
  • Alexis Saurin