Program
The program will consist of talk sessions spanning two full days on 29 and 30 September 2022.
Thursday
| 10:30-11:00: | Christian Rétoré: Proof nets and coherence spaces |
| 11:00-11:30: | Zeinab Galal: Towards 2-dimensional orthogonality |
| 11:30-12:00: | Jean-Yves Girard: Schrödinger’s cut |
| 12:00-14:00: | lunch |
| 14:00-14:30: | Pierre-Louis Curien: Condorcet meets Gustave revisited |
| At the GGJJ meeting celebrating Jean-Jacques Lévy and Gérard Berry (back in 2011), Gérard Huet explained the link between the so-called Condorcet paradox and stable functions. We recall what he presented then and complete his story with a couple of new results: we show that any abstract total relation on a finite set (viewed as a set of candidates) arises as the result of a Condorcet ballot (we shall recall the Condorcet voting system), and we characterise those Gustave functions (defined by Huet to be the stable and non sequential functions) from {bottom, true,false}^n to {bottom, top} that arise as a witness of absence of a winner of the ballot. | |
| 14:30-15:00: | Raphaëlle Crubillé |
| 15:00-15:30: | Alexandra Bac: From the geometry of proofs to the geometry of holes |
| After my PhD with Thomas Ehrhard on the denotational semantics of second order linear logic, I followed various opportunities as an Associate Professor in Marseille, leading me from the geometry of proofs to various issues related to Computer Graphics. Among other things, I’ve been working on the relations between (computational) homology and geometry. In this context, (discrete) Morse theory stands as a « strange object ». This talk will give a brief overview of this topic and sketch some results we obtained, leading to the definition of Homological Discrete Vector Fields (an extension of Discrete Morse theory). | |
| 15:30-16:00: | break |
| 16:00-16:30: | Rick Blute: Finiteness spaces and groupoids |
| Much of my recent research has been in demonstrating the idea that working with Ehrhard's notion of finiteness space forces certain sums which would a priori be infinite to become finite, and hence well-defined, without resorting to limit structure or infinitary computations. In this talk, we'll consider topological groupoids. We show that for a semigroup in the category of finiteness spaces, one can endow the R-module obtained by Ehrhard's linearization with a convolution product to obtain an R-algebra which is complete in the Lefschetz topology. In particular, for an etale groupoid whose underlying space is hemicompact we obtain a finiteness space and an internal semigroup in the category of finiteness spaces. Then by the above observation we get a convolution algebra for that groupoid, which differs from the usual algebra considered in functional analysis. | |
| 16:30-17:00: | Marie Kerjean: ∂ is for Dialectica |
| 17:00-17:30: | Giulio Manzonetto: Profunctors - what are they useful for? |
| Relational models of 𝜆-calculus can be presented as type systems, and the relational interpretation of a 𝜆-term as the set of its typings. We introduce a bicategorical model living in a distributors-induced semantics generalising the relational one, and show that it satisfies an Approximation Theorem. As in the relational case, the quantitative nature of our bicategory allows us to prove this property via a simple induction, rather than using computability predicates. Unlike relational models, our bicategorical model is also proof-relevant in the sense that the interpretation of a 𝜆-term does not contain its typings, but the whole type derivations. The additional information carried by a type derivation allows us to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterisation of the theory induced by the bicategorical model as a corollary of the Approximation Theorem: two 𝜆-terms share the same interpretation exactly when their Böhm trees coincide. | |
| 17:30-18:00: | Marcelo Fiore: The Cartesian Closed Bicategory of Cartesian Distributors |
Friday
| 09:30-10:00: | Pierre Boudes: Multicoherences |
| 10:00-10:30: | Giulio Guerrieri: The Call-by-Value Lambda-Calculus from a Linear Logic Perspective |
| Plotkin's call-by-value (CbV, for short) lambda-calculus is a variant of the lambda-calculus that models the evaluation mechanism in most functional programming languages. The theory of the CbV lambda-calculus is not as well studied as the call-by-name one, because of some technical issues due to the "weakness" of Plotkin's CbV beta-rule, which leads to a mismatch between syntax and semantics. By adopting a Curry-Howard perspective, we show how linear logic inspires several ways to solve the mismatch between syntax and semantics in CbV, paving the way for restoring a theory of the CbV lambda-calculus as elegant as the one for call-by-name. We test our approach on a type-theoretic/semantic characterization of normalizabilty and on the notion of solvability. | |
| 10:30-11:00: | break |
| 11:00-11:30: | Thomas Streicher: Thomas E.: Friend and my “Passepartout for French TCS B” for 35 years |
| 11:30-12:00: | Farzad Jafarrahmani: A concrete model of non well-founded linear logic |
| 12:00-12:30: | Antonio Bucciarelli, Laurent Regnier, Lorenzo Tortora de Falco |
|
slides for Antonio’s talk
slides for Lorenzo’s talk | |
| 12:30-14:30: | lunch |
| 14:30-15:00: | Paul-André Melliès: Strong and extensional stability through the prism of dialogue games |
| Ehrhard established in the mid-1990s that the extensional collapse of the sequential algorithm model of PCF by Berry and Curien coincides with the strongly stable model introduced with Bucciarelli a few years earlier. In this talk, I will explain how this theorem combined with the notion of hypercoherence space discovered by Ehrhard played a key role in the genesis of dialogue games and tensorial logic. I will also illustrate how strong stability as well as extensional stability can be seen through the prism of dialogue games, using a functorial translation of tensorial logic into linear logic extended with a suspension modality. | |
| 15:00-15:30: | Michele Pagani, Christine Tasson, Lionel Vaux Auclair: To finiteness spaces and beyond! |
| 15:30-16:00: | Thomas Ehrhard: Closing address |