Journées 2021 du GT Scalp

Du 3 au 5 novembre 2021 à Fontainebleau

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:

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:

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.

venir-fontainebleau.jpeg

Hébergement

Voici quelques suggestions de l'UPEC:

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

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.
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.
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.
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.
  
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.
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.
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.
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).
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.   
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.
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.
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.
(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.
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.
Combinatorial Proofs
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.
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