Journées 2021 du GT Scalp Du 3 au 5 novembre 2021 à Fontainebleau Introduction Orateurs invités Inscriptions et propositions d'exposé Informations pratiques Programme Liste des exposés Participants Important: Le mouvement social des transports en bus s'est achevé fin octobre, les bus fonctionnent à nouveau pour rejoindre l'IUT depuis la gare de Fontainebleau-Avon! (voir ci-dessous) Introduction Les rencontres 2021 du GT Scalp se dérouleront sur le campus de l'IUT de Fontainebleau de l'UPEC, et sur Internet (les informations de connexion seront envoyées aux personnes inscrites), du 3 novembre en fin de matinée jusqu'au 5 novembre en début d'après-midi. Les journées sont organisées de manière hybrides, avec participation en présence ou en visio. Les horaires des journées seront les suivants: mercredi 3 novembre: accueil le matin avec possibilité de promenade en fôret pour les personnes intéressées, exposés de 13H30 à 18H (précédés d'un déjeuner de 12H à 13H30 pour les personnes qui le souhaitent). jeudi 4 novembre: exposés 9H30 à 18H (business meeting en début d'après-midi) vendredi 5 novembre: de 9H30 à 12H30. discussions libres ou promenade en fôret pour les personnes intéressées. Les exposés invités débuteront chaque journée. Exposés invités Pour les journées 2021, les exposés invités du GT-Scalp serton donnés par: Raphaëlle Crubillé, LORIA: Applicative bisimulations for lambda-calculus with continuous probabilities; Lê Thành Dũng Nguyễn, IRISA: Implicit automata in typed λ-calculi; Gabriel Scherer, INRIA Saclay: la recherche appliquee à OCaml. Inscriptions et propositions d'exposé Pour vous inscrire ou proposer un exposé, merci de remplir le formulaire suivant qui permet à la fois de proposer un exposé et de s'inscrire aux journées. Pour participer en présence, merci de vous inscrire avant le 27 octobre. Informations pratiques Quelques informations pour vous organiser: Accès Les journées se dérouleront sur le campus de Fontainebleau de l'IUT de l'UPEC, dans le grand amphithéâtre. En transports en commun la manière la plus simple est, une fois à Paris, de prendre la ligne de Transilien R à Paris - Gare de Lyon (comme c'est une ligne de Transilien, elle se prend dans la gare — en général hall 3 — et non dans la gare souterraine) jusqu'à l'arrêt Fontainebleau – Avon (il y en a au moins un toutes les heures+16 minutes vers Fontainebleau et deux par heures dans l'autre sens <https://www.transilien.com/fr/les-fiches-horaires/>). Le trajet prend 37 minutes. Le campus est à la lisière de la forêt et du château, c'est-à-dire assez loin de la gare — 45 minutes de marche. Le mouvement social des transports en bus s'est achevé fin octobre, les bus fonctionnent à nouveau pour rejoindre l'IUT! De la gare de Fontainebleau-Avon, prendre le bus ligne 1 à la gare routière (la gare routière se trouve le long du quai arrivant de Paris, l'arrêt de la ligne 1 est le “quai 1, vers le château de Fontainebleau”) en direction des Lilas, jusqu'au terminus: Horaires en temps réel des bus de la ligne 1 de la gare routière de Fontainebleau-Avon vers l'IUT. (indique les heures de départ des prochains bus ainsi que, par défaut, les horaires de la journée du mercredi 3 novembre 2021) Fiche horaire et plan de la ligne 1. Hébergement Voici quelques suggestions de l'UPEC: Hôtel Richelieu Bacchus de Fontainebleau Hôtel IBIS de Fontainebleau Programme Mercredi 3 novembre 10:00 - 10:30 accueil des premiers arrivants 10:30 - 12:00 sortie en forêt pour les personnes volontaires (prévenir à l'avance si intéressées) 12:00 accueil et déjeuner 13:30 ouverture des journées Scalp Session M1 (chairs: Pierre Clairambault & Luc Pellissier) 13:40 Lê Thành Dũng Nguyễn, Implicit automata in typed λ-calculi 14:30 Farzad Jafarrahmani, A concrete model of finitary/infinitary linear logic with fixed-points 14:55 Anupam Das, A circular version of Gödel's T and its abstraction complexity 15:20 Gianluca Curzi, Cyclic Implicit Complexity 15:45 pause café et discussions libres Session M2 (chair: Jules Chouquet) 16:45 Kostia Chardonnet, Geometry of Interaction for ZX-Diagrams 17:10 Boris Eng, Transcendental Syntax: a toolbox for the interface logic-computation 17:35 Alexis Ghyselen, Types for Complexity of Parallel Computation in Pi-Calculus 18:00 discussions libres et apéritif Jeudi 4 novembre Session J1 (chair: Chantal Keller) 09:30 Raphaëlle Crubillé, Applicative bisimulations for lambda-calculus with continuous probabilities 10:20 Ambroise Lafont, Substitutional variable binding for the (nameless) dummies 10:45 pause café et discussions libres Session J2 (chair: Jean-Marie Madiot) 11:45 Pierre Vial, Snipe: when Bécassine brings automation to Coq 12:10 Rébecca Zucchini, Formalisation en Coq de la provenance des données en bio-informatique 12:35 déjeuner 13:35 Business meeting Session J3 (chair: Simon Castellan) 14:45 Lison Blondeau, Positional Injectivity for Innocent Strategies 15:10 Guilhem Jaber, Modular Operational Nominal Game Semantics 15:35 pause café et discussions libres Session J4 (chair: Ambroise Lafont) 16:45 Samuel Mimram, A cartesian bicategory of polynomial functors in homotopy type theory 17:10 Louis Lemonnier, Categorical Semantics of Reversible Pattern-Matching 17:35 Ralph Matthes, Implementing a category-theoretic framework for typed abstract syntax 18:00 discussions libres et apéritif Vendredi 5 novembre Session V1 (chair: Kenji Maillard) 09:30 Gabriel Scherer, la recherche appliquée à OCaml. 10:20 Victor Arrial, Inhabitation in Call-by-Push-Value 10:45 pause café et discussions libres Session V2 (chair: Delia Kesner) 11:55 Sergueï Lenglet, Non-Deterministic Abstract Machines 12:20 Lutz Strassburger, Combinatorial Proofs 12:45 clôture des journées et déjeuner 14:00 - 16:00 discussions libres ou sortie en forêt pour les personnes intéressées Liste des exposés contribués Victor Arrial, Inhabitation in Call-by-Push-Value Nous étudions le problème d'inhabitation (synthèse de programmes) dans le Call-by-Push-Value avec un système de typage à Intersections non-Idempotentes (Bang-calculus), présentant un algorithme pour le décider. Nous explorons par la suite les restrictions de cet algorithme aux images des encodages Call-by-Name et Call-by-Value afin d'en résoudre les problèmes d'Inhabitation correspondants. Pour finir, nous comparons ces résultat aux différents algorithmes de la littérature. Lison Blondeau, Positional Injectivity for Innocent Strategies In asynchronous games, Melliès proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics. In this talk, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. We show that though innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions. Cet exposé se base sur un article co-écrit avec Pierre Clairambault. Kostia Chardonnet, Geometry of Interaction for ZX-Diagrams ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this work we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams. Gianluca Curzi, Cyclic Implicit Complexity Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common 'recursion schemes'. This talk attempts to bridge the gap between circular proofs and implicit computational complexity. Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify suitable proof theoretical constraints to characterise the polynomial-time and elementary computable functions. Anupam Das, A circular version of Gödel's T and its abstraction complexity Circular and non-wellfounded proofs have become an increasingly popular tool for metalogical treatments of systems with forms of induction and/or recursion. In this work we investigate the expressivity of a variant CT of Gödel's system T where programs are circularly typed, rather than including an explicit recursion combinator. In particular, we examine the abstraction complexity (i.e. type level) of CT, and show that the Gödel primitive recursive functionals may be typed more succinctly with circular derivations, using types precisely one level lower than in T. In fact we give a logical correspondence between the two settings, interpreting the quantifier-free type 1 theory of level n+1 T into that of level n CT and vice-versa. We also obtain some further results and perspectives on circular 'derivations', namely strong normalisation and confluence, models based on hereditary computable functionals, continuity at type 2, and a translation to terms of T computing the same functional, at all types. Boris Eng, Transcendental Syntax: a toolbox for the interface logic-computation I present the Transcendental Syntax, a programme recently introduced by Girard which I formalised with Thomas Seiller. In this programme, a new model of computation I call "stellar resolution" is used as elementary bricks. It is able to naturally represent state machines, circuits, logic programs and tile systems in an uniform way. From this model of computation, Girard suggested to define linear logic as emerging from computation instead of defined from primitive constructions. Instead of linear logic, I will focus on how the Transcendental Syntax introduces a notion of unit testing in logic and sketch how it could be used as a toolbox for designing types. Alexis Ghyselen, Types for Complexity of Parallel Computation in Pi-Calculus Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular some systems allow to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of the pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions, and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by size types and by input/output types, with additional temporal information about communications. Guilhem Jaber, Modular Operational Nominal Game Semantics In this talk, we will see how to build fully abstract trace models of programming languages in a systematic way using labelled transition systems designed by operational game semantics. We will consider programming languages with features that include memory operators (local references), control operators (call/cc), cryptographic operators (dynamic sealing), and rich type systems (algebraic data types, parametric polymorphism). Farzad Jafarrahmani, A concrete model of finitary/infinitary linear logic with fixed-points We provide two denotational semantics of finitary/infinitary full propositional classical linear logic extended with least and greatest fixpoints of formulae in the relational model (REL) and non-uniform totality spaces (NUTS). Those models interpret the least and greatest fixed-point operators (mu and nu resp.) in different ways: mu and nu are interpreted in the same way in REL while their interpretations are different in NUTS, though the proofs are interpreted by the same sets in both models. Finally, in the case of infinite proofs, we show that the interpretation of a valid proof is a total element. Ambroise Lafont, Substitutional variable binding for the (nameless) dummies Joint work with Andre & Tom Hirschowitz, Marco Maggesi. We propose an initial-algebra semantics framework for syntax with variable binding inspired by De Bruijn representation with nameless dummies. Following Fiore, Plotkin, and Turi, our framework is substitutional, in the sense that models all come equipped with a substitution operation. It is however more elementary than their presheaf-based framework. Our framework can accomodate simple types, equations between terms, and a transition relation. Louis Lemonnier, Categorical Semantics of Reversible Pattern-Matching This talk is concerned with categorical structures for reversible computation. In particular, we focus on a typed, functional reversible language based on Theseus. We discuss how join inverse rig categories do not in general capture pattern-matching, the core construct Theseus uses to enforce reversibility. We then derive a categorical structure to add to join inverse rig categories in order to capture pattern-matching. We show how such a structure makes an adequate model for reversible pattern-matching. Sergueï Lenglet, Non-Deterministic Abstract Machines We present a generic design of abstract machines for non-deterministic programming languages such as process calculi or concurrent lambda calculi. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way. We show how to automatically derive a non-deterministic abstract machine from a zipper semantics---a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics. Ralph Matthes, Implementing a category-theoretic framework for typed abstract syntax (joint work with Benedikt Ahrens and Anders Mörtberg) Recently, we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant. In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply-typed case. Second, an existing mechanized library on omega-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, and most excitingly, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bicategorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using the recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly. The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation. Samuel Mimram, A cartesian bicategory of polynomial functors in homotopy type theory Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections. This is joint work with Eric Finster, Maxime Lucas and Thomas Seiller. Lutz Strassburger, Combinatorial Proofs Combinatorial Proofs Pierre Vial, Snipe: when Bécassine brings automation to Coq We present a new Coq tactic, snipe (la bécassine des marais in french), which allows automatically solving goals in Coq by sending them to external (automated) first-order theorem provers. Snipe reduces the goal to a first-order statement (if possible) and proves in the local context various useful first-order logic statements which help making the semantic of the goal explicit for the external prover. We combine modular and independent transformations: each one of them reduces a specific aspect of the logic of Coq to the (simpler) logic of an automated prover. Currently, snipe implements simple but crucial transformations which unfold definitions of functions and algebraic types. This allows automatically solving goals by mixing first-order reasoning with datatypes and polymorphism. Snipe is a first step towards implementing and combining more complex transformations, which will help bringing more automation to Coq and making it more accessible for wide use. Rébecca Zucchini, Formalisation en Coq de la provenance des données en bio-informatique Je souhaiterais proposer un exposé sur mon sujet de thèse. Cette thèse consiste à formaliser dans l'assistant de preuve Coq, la provenance des données dans le cadre particulier de la bio-informatique. Avec une production de données brutes toujours plus intense et des traitements s’effectuant sur des jeux de données de plus en plus conséquents, il y a un risque de perdre le sens des résultats obtenus et d’introduire des erreurs d’interprétation de ceux-ci. Il est donc crucial d’apporter plus de confiance dans le traitement de larges ensembles de données. La provenance est une notion issue du monde des bases de données et est fondée sur des mécanismes de traçage et d’annotation des données. Elle peut être relative à trois informations : à l’origine des données résultantes (where-provenance), aux raisons pour lesquelles nous obtenons une donnée (why-provenance) ou à celles qui expliquent l’absence d’un résultat (why-not-provenance). Bien que de nombreuses communautés aient aujourd’hui conscience de l’importance de la provenance, aucune approche n’a jusqu’alors été proposée pour garantir formellement la provenance d’un résultat obtenu par une analyse de données. Pour remédier à cela, nous proposons dans cette thèse une formalisation en Coq de deux types de provenance des données dans le cadre d’une algèbre relationnelle. Participants Matteo Acclavio Victor Arrial Stephane Aubry Davide Barbarossa Nicolas Blanco Lison Blondeau-Patissier Simon Castellan Félix Castro Kostia Chardonnet El Mehdi Cherradi Jules Chouquet Pierre Clairambault Norbert Cot Raphaëlle Crubillé Gianluca Curzi Anupam Das Abhishek De Louise Dubois de Prisque Aloÿs Dufour Boris Eng Hugo Férée Laura Fontanella Alexis Ghyselen Marianna Girlando Stefano Guerrini Guilhem Jaber Farzad Jafarrahmani Chantal Keller Axel Kerinec Delia Kesner Ambroise Lafont Dongho Lee Louis Lemonnier Sergueï Lenglet Jean-Marie Madiot Kenji Maillard Ralph Matthes Damiano Mazza Samuel Mimram Marianela Evelyn Morales Elena Guillaume Munch-Maccagnoni Nicolas Munnich Tito Nguyen Rémi Nollet Giti Omidvar Romain Péchoux Luc Pellissier Elaine Pimentel Colin Riba Alexis Saurin Gabriel Scherer Léo Stefanesco Lutz Strassburger Pierre Valarcher Lionel Vaux Auclair Pierre Vial Rébecca Zucchini