• Introduction
• Oratrices et orateurs invités
• Inscriptions et propositions d'exposé
• Informations pratiques
• Programme
• Liste des exposés contribués
• Participant·es
• Comité d'organisation

Les rencontres 2025 du GT Scalp se tiendront à Vitry-sur-Seine du 27 au 29 octobre.

Cette année, les rencontres sont organisées par nos collègues du LACL (UPEC) et se tiendront à l'IUT de Vitry-sur-Seine (amphi Chimie).

Les informations sur les exposés invités et contribués ainsi que sur l'organisation pratique des journées seront progressivement complétées ci-dessous.

• Thérèse Hardin (Pr. émérite, LIP6, Université Sorbonne Université), rendra hommage à Gilles Dowek en nous présentant son ouvrage «Ce livre dont on ne peut parler, il faut l’écrire»
• Miriam Backens (C.R. INRIA, LORIA) fera un tutoriel et un exposé sur l'informatique quantique et le ZX-calculus.
• Gabriele Vanoni (post-doct., IRIF, Université Paris Cité) nous dira comment compiler des programmes probabilistes vers des circuits quantiques (en anglais)

L'inscription est gratuite mais obligatoire. Le formulaire d'inscription est disponible ici

https://framaforms.org/journees-scalp-2025-1756825325

Lors de l'inscription, vous serez invités à préciser à quelles demi-journées vous souhaitez participer et si vous souhaitez proposer un exposé et/ou un atelier. L'inscription couvre également les repas du mardi midi et du mercredi midi.

L'inscription doit se faire au plus tard le 5 octobre.

Cette année il sera possible de contribuer au programme des journées de différentes manières (non exclusives) :

• proposer un exposé de recherche (toute les thématiques du GT sont les bienvenues !)
• proposer un exposé tutoriel (pour renforcer nos connaissances communes)
• proposer un atelier ou un groupe de discussion informel, portant sur des travaux en cours ou sur d'autres aspects liés à la recherche (organisation du GT, les candidatures, le travail de chercheureuse, interaction science et société, …)

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

L'objectif des ateliers est de favoriser les échanges au sein du GT en proposant un format interactif permettant par exemple de discuter de travaux en cours ou d'échanger sur nos pratiques de la recherche. Les ateliers feront l'objet d'une courte présentation en plénière puis se dérouleront lors d'une session en parallèle, de manière libre, aux choix des participant·e·s. Sur demande des intervenant·e·s, de l'aide pourra être apportée pour médier les interactions.

Afin de refléter la richesse de la communauté Scalp, toute proposition de contributions est bienvenue !

Comme d'habitude nous demandons aux encadrant·es d'encourager leurs encadré·es à présenter leurs travaux. Cela n'empêche pas les chercheureuses plus senior de proposer également des interventions ou de venir assister aux journées afin que les jeunes chercheureuses puissent s'intégrer plus facilement dans la communauté.

Les rencontres se dérouleront à Vitry dans les locaux de l'IUT de Créteil-Vitry (principalement en amphi de Chimie) :

122 Rue Paul Armangot, 94400 Vitry-sur-Seine. (plan d'accès)

En transport en commun :

• Tram T7 arrêt Domaine Chérioux. Il suffit ensuite de traverser le parc (se reporter au plan d'accès car les GPS ne connaissent pas le chemin)
• Bus 185 arrêt Paul Armangot.
• Métro 7 arrêt Villejuif - Louis Arragon. Continuer à pied ou faire une correspondance avec le tram T7 ou le bus 185.

En voiture : Un parking se situe juste à côté de l'IUT

• Hotel Ibis Orly Chevilly Tram 7 (directement en face du domaine Cherioux)
• Ibis Styles Paris-Villejuif, Hôtel Grand Paris (20 minutes à pied, 10 par le tram ; proximité du centre de Villejuif plus animé que les abords de l'IUT)
• Dans Paris, le long de la ligne 7 jusqu'à la place d'Italie (30 minutes de transports en métro + bus)

• Ambiance Asie (Vietnamien) 30 Rue Georges Lebigot, 94800 Villejuif
• Crêperie l'Hirondelle 32 Rue Georges Lebigot, 94800 Villejuif
• Maihak (Indien) 102 Rue Jean Jaurès, 94800 Villejuif
• Show Devant (Bistrot) 38 Rue Georges Lebigot, 94800 Villejuif
• Tassili (Couscous et Tajine) 85 Rue Jean Jaurès, 94800 Villejuif

Les journées se dérouleront du lundi 27 octobre à 13h au mercredi 29 octobre à 13h. Le programme est le suivant:

• Lundi 27 octobre après-midi (à partir de 13h)
  • 13h00-13h30: Café de bienvenue
  • 13h30-14h30: Tutoriel invité, Miriam Backens
  • 14h30-15h00: Victor Sannier
  • 15h00-15h30: Tomas Vallejos Parada
  • 15h30-16h00: Pause
  • 16h00-16h30: Tutoriel, Guilhem Jaber
  • 16h30-17h00: Sidney Congard
  • 17h00-17h30: Colin Riba
  • 17h30-18h00: Ralph Matthes
  • 18h00-18h15: Présentations ateliers

• Mardi 28 octobre
  • 8h30-9h30: Exposé invité, Miriam Backens
  • 9h30-10h00: Eléonore Mangel
  • 10h00-10h30: Iwan Quémerais
  • 10h30-11h00: Pause
  • 11h00-11h30: Simon Castellan
  • 11h30-12h00: Victoria Barrett
  • 12h00-12h30: Ada Picano-Nacci
  • 12h30-14h00: Déjeuner
  • 14h00-14h30: Tutoriel, Ralph Sarkis
  • 14h30-15h00: Thomas Traversié
  • 15h00-15h30: Exposé invité, Thérèse Hardin
  • 15h30-16h00: Pause
  • 16h00-17h30: Ateliers
  • 17h30-18h30: Infos GdR et GT Scalp puis discussion politique

• Mercredi 29 novembre
  • 8h30-9h30: Exposé invité, Gabriele Vanoni
  • 9h30-10h00: Thibaut Balabonski
  • 10h00-10h30: Stefano Catozi
  • 10h30-11h00: Pause
  • 11h00-11h30: Adrienne Lancelot
  • 11h30-12h00: Rémi Di Guardia
  • 12h00-12h30: Ralph Sarkis
  • 12h30-13h00: Gabriel Scherer
  • 13h00-14h00: Déjeuner

• Thibaut Balabonski, Lambda-calcul et complexité spatiale. Slides Abstract

  We propose a simple space-cost model for the λ-calculus and prove that, in the context of weak reduction, this model is reasonable with respect to standard space complexity theory. Precisely, we show that the weak λ-calculus and Turing machines can simulate each other with a constant factor overhead in space complexity, as long as this complexity is at least logarithmic. This implies that the weak λ-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including Logspace and Pspace. (more).
• Victoria Barrett, Proof normalisation and compression with explicit substitutions.
• Simon Castellan, Lazy evaluation of probabilistic programs on algebraic data types. Slides Abstract

  In this talk, I will present how to compute efficiently the distribution semantics of a first-order programs, by relying on an intermediate representation based on binary decision diagram. The approach rests on the fact that for these BDDs, call-by-name evaluation and call-by-value evaluation coincide and so call-by-name can be used to speed up evaluation.
• Stefano Catozi, On Jumps, Interactions, and Intersections.
• Sidney Congard, Une correspondance Curry-Howard pour les destructeurs en C++. Abstract

  We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad in a linear setting. We consider in particular for the allocation monad, which we introduce to model and study resource-safety properties. We apply these results to two linear effectful calculi for which we establish their resource-safety properties. (more)
• Rémi Di Guardia, Confluence of Cut-elimination and Rules commutations in Linear Logic. Slides Abstract

  This talk studies the identity of proofs: when are two proofs equal? Generally, syntactic equality is too constraint, and one wants to (at least) identify proofs up to cut-elimination - which is similar to identifying λ-terms up to β-reduction. We begin by giving intuitions for this problem in simply typed λ-calculus, where it is easily solved thanks to strong normalization and confluence of β-reduction. Then, we see which problems arise when trying to mimic this reasoning in Linear Logic. The main difficulty is that cut-elimination is only confluent up to an equivalence relation known as rule commutations, which is not easy to prove. We conclude by showing that knowing whether two given proofs are equal up to rule commutations, or not, is undecidable.
• Adrienne Lancelot, Constructive Contextual Equivalence.
• Eléonore Mangel, Classical notions of computation and the Hasegawa-Thielecke theorem. Slides
• Ralph Matthes, Data-type aware reconstruction of dynamical method. Slides Abstract

  The dynamical method in the sense of Michel Coste, Henri Lombardi and Marie-Françoise Roy, as published in a 2001 APAL paper, is a blend of proof-theoretic methods at the service of obtaining constructive results in algebra. That ground-breaking paper aims at uses of the method for variations of Hilbert's Nullstellensatz. The method itself is not the focus of that paper. We are revisiting the method in the light of theoretical computer science, in particular by exhibiting the data structures underlying the dynamical method. We give a Curry-Howard style reformulation of the notion of dynamical proof, permitting transparent proofs of the admissibility of the logical rules for disjunction, existential quantification and classical negation. The culture of abstract data-types also drives our examination of the notions of algebraic certificates that are at the heart of the proofs in the aforementioned paper of admissibility of, e.g., the axiom expressing algebraic closure of a field - admissibility being expressed as preservation of theory collapse. This is joint work with Stefan Neuwirth (Univ. Marie et Louis Pasteur, but the work has been performed during his leave to the IRIT).
• Ada Picano-Nacci, Réalisabilité classique pour la théorie des ensembles, Ultraséparateurs génériques et témoins
• Iwan Quémerais, First-order Store and Visibility in Name-passing calculi
• Colin Riba, Toward Refinement Types for Temporal Properties in Scott Domains. Abstract

  We are interested in proving input-output properties of functions that handle infinite data such as streams (or non-wellfounded trees). At the level of denotational semantics, we build from the well-known fact that the Scott domains interpreting recursive types are Spectral spaces. We work on top of Stone duality, following Abramsky's Domain Theory in Logical Form (1987, 1991). In this setting, saturated properties (ie upward-closed subsets) encompass an interesting range of temporal properties, including least and greatest fixpoints of negation-free formulae. As expected, usual safety properties turn out to be compact saturated sets of streams (while they are closed sets in the usual topology of omega-words). Further, a sound and complete infinitary refinement type system for saturated properties, inspired from Bonsangue and Kok (2003), allows for proving input-output specifications of functions on recursive types. We will also outline recent works on a finitary refinement type system which is sound and complete for a family of infinitary Scott-open properties which includes alternation-free least fixpoints of negation-free formulae. Jww Solal Stern, Alexandre Kejikian and Adam Donadille.
• Victor Sannier, Un système de types avec coeffets dépendants pour analyser la sensibilité locale. Abstract

  La confidentialité différentielle borne la fuite d'information maximale que l'on peut accepter lors de requêtes sur des données sensibles. Pour la garantir, on peut borner la sensibilité de la requête (l'impact des variations d’entrée sur la sortie) et ajouter un bruit proportionnel à cette sensibilité. Les systèmes de types linéaires comme Fuzz ciblent la sensibilité globale, souvent infinie pour des requêtes utiles, limitant leur portée. Dans cet exposé, je présente Local Fuzz, un système de types à coeffets gradués type-dépendants qui borne la sensibilité locale. Nous donnons une sémantique dénotationnelle via la catégorie des espaces prémétriques étendus et une comonade dépendamment graduée. Local Fuzz offre ainsi de meilleures garanties que Fuzz pour des mécanismes fondés sur la sensibilité locale, tels que Propose-Test-Release, et même pour des mécanismes fondés sur la sensibilité globale.
• Ralph Sarkis, Towards Quantitative Diagrammatic Reasoning. Slides Abstract

  Algebraic reasoning has been popular in the study of program semantics but it cannot model two important features. Quantitative reasoning, namely, studying distances between programs instead of equivalences and resource sensitivity, namely, keeping track of how processes and results are copied, discarded, and reused. The solution we propose is to reason (compositionally) about distances between string diagrams by extending the work on quantitative algebraic reasoning (Mardare et al. 2016) to monoidal terms. We apply this approach to the total variation distance between stochastic matrices.
• Gabriel Scherer, L'inférence à la ML dans tous les sens. Slides.
• Thomas Traversié, Traductions entre logiques d'ordre supérieur à l'aide de monades. Slides.
• Tomas Vallejos Parada, Proving Pornin's modular inversion algorithm correct in Why3.

• Guilhem Jaber, The full-abstraction problem for System F
• Ralph Sarkis, String Diagrams for Computer Scientists Slides Abstract

  String diagrams are a well-established graphical syntax for morphisms in monoidal categories. They have become popular in many areas of computer science because monoidal categories are often the correct structure to describe a class of processes or systems. We will see what string diagrams are and how they can be seen as inductively generated syntax for several semantics (e.g. functions, matrices, regular languages).

• Simon Castellan, Logiques et sémantiques à l'heure des urgences socio-environementales: Science de Domination ou Science d'Émancipation
• Lê Thành Dũng (Tito) Nguyễn, What future for our conferences? Let's discuss our publishing and networking models
• Ralph Sarkis, Teaching higher mathematics to high school students using string diagrams

• Aurore Alcolei
• Hong-Linh ANH-TON-LE (il/lui)
• Thibaut Antoine (il/iel)
• Miriam Backens (gender-neutral terms)
• Thibaut Balabonski
• Victoria Barrett (she/her)
• Victor Blanchi (Il)
• Simon Castellan (Il)
• Stefano Catozi
• Rémy Cerda
• Kostia Chardonnet
• Pierre Clairambault
• Emily Clement (Elle)
• Sidney Congard (Il)
• Rémi Di Guardia
• Ivan Doubovik
• Aloÿs Dufour (Il)
• Noé Ensarguet (he/him)
• Thérèse Hardin
• Elies Harington (Il/Lui)
• Hugo Herbelin (Il)
• Olivier Hermant
• Guilhem Jaber (iel)
• Chantal Keller
• Axel Kerinec (il/lui)
• Delia Kesner
• Adrienne Lancelot
• Thomas Laure (il/lui)
• Serge Lechenne
• Sergueï Lenglet
• Eléonore Mangel
• Ralph Matthes (he/him)
• Damiano Mazza (Il/lui)
• Guillaume Munch-Maccagnoni
• Lê Thành Dũng (Tito) Nguyễn (he/him)
• Federico Olimpieri
• Hugo Paquet
• Romain Péchoux
• Luc Pellissier (lui/il)
• Ada PICANO-NACCI (Elle + accords féminins)
• Iwan Quémerais (any)
• Colin Riba
• Victor Sannier
• Ralph Sarkis (he/him (il/lui))
• Gabriel Scherer
• Artur Szafarczyk
• Thomas Traversié (Il/lui)
• Emilie Uthaiwat (Elle)
• Tomas Vallejos Parada (He/him)
• Gabriele Vanoni (Il)
• Thomas VINET

Comité d'organisation des journées du GT Scalp:

• Aurore Alcolei (LACL, UPEC)
• Pierre Clairambault (Scalp)
• Chantal Keller (Scalp)
• Luc Pellissier (LACL, UPEC)
• Alexis Saurin (Scalp)
• Pierre Valarcher (LACL, UPEC)