===== Journées 2021 du GT Scalp =====
==== Du 3 au 5 novembre 2021 à Fontainebleau ====
* [[gt-scalp:journees-2021#introduction|Introduction]]
* [[gt-scalp:journees-2021#orateurs_invites|Orateurs invités]]
* [[gt-scalp:journees-2021#inscriptions_et_propositions_d_expose|Inscriptions et propositions d'exposé]]
* [[gt-scalp:journees-2021#informations_pratiques|Informations pratiques]]
* [[gt-scalp:journees-2021#programme|Programme]]
* [[gt-scalp:journees-2021#liste_des_exposes|Liste des exposés]]
* [[gt-scalp:journees-2021#participants|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 [[http://www.irif.fr/gt-scalp/|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:
* [[http://research.crubille.lautre.net/|Raphaëlle Crubillé]], LORIA: [[https://www.irif.fr/_media/gt-scalp/raphaelle-crubille.pdf|Applicative bisimulations for lambda-calculus with continuous probabilities]];
* [[https://nguyentito.eu/|Lê Thành Dũng Nguyễn]], IRISA: [[https://www.irif.fr/_media/gt-scalp/tito-nguyen.pdf|Implicit automata in typed λ-calculi]];
* [[http://www.lix.polytechnique.fr/Labo/Gabriel.Scherer/|Gabriel Scherer]], INRIA Saclay: [[https://www.irif.fr/_media/gt-scalp/gabriel-scherer.pdf|la recherche appliquee à OCaml]].
==== Inscriptions et propositions d'exposé ====
Pour vous inscrire ou proposer un exposé, merci de remplir le
**[[https://framaforms.org/journees-scalp-2021-1630651447|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**.
/*
[[https://framaforms.org/gt-scalp-rencontres-2019-18-octobre-a-lyon-inscription-1567505861|formulaire suivant]].
*/
==== 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. ([[https://www.iutsf.u-pec.fr/l-iut/comment-venir#venir_a_fontainebleau|Informations pour venir à Fontainbleau]].)
*/
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
). 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:
/*
Par ailleurs les personnels de la
compagnie de bus assurant le service à Fontainebleau sont en ce moment en grève
du fait de la renégociation des délégations de service public avec Île-de-France
Mobilités. **Nous allons organiser du covoiturage de minibus depuis la gare.**
*/
[[https://www.transdev-idf.com/horaires-ligne-1/gare-routiere-quai-1-vers-les-lilas/062-URB-50017411-50017582?date=03-11-2021&stationdropoff=50017582|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)
[[https://www.transdev-idf.com/api/1.0/timetablefile/753726307/raw/ligne_1-7_volets_2plis_bat2.pdf|Fiche horaire et plan de la ligne 1.]]
{{venir-fontainebleau.jpeg?1000}}
/*
== Événement social ==
Pour l'événement social du GT, nous proposons cette année une visite nocturne au musée des confluences le jeudi 17 au soir.
*/
== Hébergement ==
/*
[[http://www.ens-lyon.fr/LIP/index.php/useful-informations#Hotels|Liste d'hôtels]] et [[http://www.ens-lyon.fr/LIP/index.php/useful-informations#Restaurants|de restaurants]] suggérés par le LIP.
Information à venir.
*/
Voici quelques suggestions de l'UPEC:
* [[https://www.richelieu-fontainebleau.com/| Hôtel Richelieu Bacchus de Fontainebleau]]
* [[https://all.accor.com/hotel/1028/index.fr.shtml| Hôtel IBIS de Fontainebleau]]
==== Programme ====
/*
Information à venir.
*/
=== 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 ===
/*
[[https://www.irif.fr/_media/gt-scalp/bm.pdf|bm]]
*/
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
/*
* Jeudi 17 octobre: exposés invités ([[https://www.cs.bham.ac.uk/~drg/|Dan Ghica]] et [[https://sites.google.com/site/valeriavignudelli/|Valeria Vignudelli]]) en lien avec le [[http://chocola.ens-lyon.fr/|séminaire Chocola]] (et soutenance de thèse d'Aurore Alcolei).
* Vendredi 18 octobre: exposés contribués. La journée devrait se dérouler de 9H à environ 17H/17H30 (légères modifications encore possible sur les horaires.)
Voici un version préliminaire du programme, encore susceptible de subir de quelques ajustements:
=== Jeudi 17 octobre ===
À l'ENS Lyon
== Session 1 ==
14h-15h: Dan Ghica (invited talk). The next 700 abstract machines
== Session 2 ==
15h30–16h30: Valeria Vignudelli (invited talk). The Theory of Traces for Systems with Nondeterminism and Probability
=== Vendredi 18 octobre: ===
En amphi G1, ISFA **(cf informations pratiques, ci-dessus)**
8h30-9h: Accueil (informel)
== Session 3 ==
Modération: Laurent Régnier
9h-9h20: Karim Nour. Normalisation en lambda mu mu'- calcul
9h25-9h45: Loïc Peyrot. Types quantitatifs pour le lambda-calcul atomique
9h50-10H10: Federico Olimpieri. Rigid intersection types as generalized species: a bi-categorical model for pure lambda-calculus.
10h15-10h45: Pause
== Session 4 ==
Modération: Amina Doumane
10h45-11h05: Abhishek De. Towards Circular Proof Nets
11h10-11h30: Rémi Nollet. PSPACE-completeness of the thread criterion for circular proofs in MALL with least and greatest fixed points.
11h35-11h55: Laureline Pinault. Cyclic proofs and Jumping automata
12h - 13h30: Déjeuner
== Session 5 ==
13h30-14h30: Business Meeting
Modération: Délia Kesner
14h30-14h50: Claudia Faggian. Factorize your way to normalization (and beyond)
14h55-15h15: Lionel Vaux. The algebraic λ-calculus, 12 years later: a conservativity proof at last
15h20-15h45: Pause
== Session 6 ==
Modération: Valentin Blot
15h45-16h05: Olivier Laurent. The Logic of Phase Semantics
16h10-16h30: Christian Retoré. Completeness of first order intuitionistic logic with respect to (pre)sheaves of classical models
16h35-16h55: François Thiré. Interoperability between Cumulative Type Systems
17h15: Fin des journées
*/
==== Liste des exposés contribués ====
* Victor Arrial, [[https://www.irif.fr/_media/gt-scalp/victor-arrial.pdf|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, [[https://www.irif.fr/_media/gt-scalp/lison-bondeau.pdf|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, [[https://www.irif.fr/_media/gt-scalp/kostia-chardonnet.pdf|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, [[https://www.irif.fr/_media/gt-scalp/gianluca-curzi.pdf|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, [[https://www.irif.fr/_media/gt-scalp/anupam-das.pdf|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, [[https://www.irif.fr/_media/gt-scalp/boris-eng.pdf|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, [[https://www.irif.fr/_media/gt-scalp/alexis-ghyselen.pdf|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, [[https://www.irif.fr/_media/gt-scalp/guilhem-jaber.pdf|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, [[https://www.irif.fr/_media/gt-scalp/farzad-jafarrahmani.pdf|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, [[https://www.irif.fr/_media/gt-scalp/ambroise-lafont.pdf|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, [[https://www.irif.fr/_media/gt-scalp/louis-lemonnier.pdf|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, [[https://www.irif.fr/_media/gt-scalp/serguei-lenglet.pdf|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, [[https://www.irif.fr/_media/gt-scalp/ralph-matthes.pdf|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, [[https://www.irif.fr/_media/gt-scalp/samuel-mimram.pdf|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, [[https://www.irif.fr/_media/gt-scalp/pierre-vial.pdf|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, [[https://www.irif.fr/_media/gt-scalp/rebecca-zucchini.pdf|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.
/*
* Abhishek De. Towards Circular Proof Nets
* Claudia Faggian. Factorize your way to normalization (and beyond)
* Olivier Laurent. The Logic of Phase Semantics
* Paul-André Melliès. Template games and differential linear logic (annulé)
* Rémi Nollet. PSPACE-completeness of the thread criterion for circular proofs in MALL with least and greatest fixed points.
* Karim Nour. Normalisation en lambda mu mu'- calcul
* Federico Olimpieri. Rigid intersection types as generalized species: a bi-categorical model for pure lambda-calculus.
* Loïc Peyrot. Types quantitatifs pour le lambda-calcul atomique
* Laureline Pinault. Cyclic proofs and Jumping automata
* Christian Retoré. Completeness of first order intuitionistic logic with respect to (pre)sheaves of classical models
* François Thiré. Interoperability between Cumulative Type Systems
* Lionel Vaux. The algebraic λ-calculus, 12 years later: a conservativity proof at last
*/
==== Participants ====
/*
Information à venir.
*/
* 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