Je suis doctorant contractuel à l'Université d'Aix-Marseille, au sein de l'équipe Logique de la programmation de l'Institut de mathématiques de Marseille (I2M, UMR 7373).

I'm a PhD student at Aix-Marseille University, in the Logics of Programming team of the Mathematics Institute of Marseille (I2M, UMR 7373).

Je m'intéresse principalement aux fondements mathématiques de l'informatique. Mes travaux de thèse s'inscrivent dans la théorie de la démonstration, qui consiste à formaliser et à étudier la notion de preuve mathématique, notamment au travers de la correspondance preuves-programmes qui permet de doter les preuves d'un contenu calculatoire.

I'm mainly interested in the mathematical foundations of computer science. My PhD work belongs to proof theory, that is the formalisation and the study of the notion of mathematical proof, in particular in the context of the proofs-as-programs correspondence that allows to endow the proofs with a computational content.

À côté de ça j'enseigne les mathématiques et l'informatique, j'ai aussi fait un peu de sciences sociales sur des questions liées à l'enseignement des mathématiques, et je m'occupe de quelques autres bricoles.

Apart from that I teach mathematics and computer science, I also did a little social sciences around questions related to the teaching of mathematics, and I'm tinkering with some other things.

Recherche Research

Ma thèse, préparée depuis septembre 2020 sous la direction de Lionel Vaux Auclair et Laurent Regnier, porte sur l'étude du λ-calcul infinitaire à l'aide d'outils issus de la sémantique quantitative, notamment le développement de Taylor des λ-termes. L'objectif de ce travail est de contribuer à décrire, à approximer et à caractériser le comportement calculatoire de termes (de « programmes ») qui ne terminent pas nécessairement.

I prepare my PhD since September 2020 under the supervision of Lionel Vaux Auclair and Laurent Regnier. It deals with the study of the infinitary λ-calculus using tools from quantitative semantics, in particular the Taylor expansion of λ-terms. The goal of this work is to contribute to describing, approximating and characterising the computational behaviour of terms (or “programs”) that do not necessarily terminate.

Avant ça, j'ai suivi une double formation en mathématiques et en informatique théorique, et j'ai notamment aimé jouer avec des types dépendants et des catégories.

Prior to this, I studied both mathematics and computer science, and I had fun playing in particular with dependent types and categories.

Je participe également aux groupes de travail LHC et SCALP du groupement de recherche Informatique mathématique du CNRS.

I participate in the LHC and SCALP working groups of the CNRS groupement de recherche Informatique mathématique.

Travaux

Published work

R.C. et L. Vaux Auclair, How To Play The Accordion. On the (Non-)Conservativity of the Reduction Induced by the Taylor Approximation of λ-Terms (brouillon).

RésuméPDFarXiv

The Taylor expansion, which stems from Linear Logic and its differential extensions, is an approximation framework for the λ-calculus (and many of its variants). The reduction of the approximants of a λ-term induces a reduction on the λ-term itself, which enjoys a simulation property: whenever a term reduces to another, the approximants reduce accordingly. In recent work, we extended this result to an infinitary λ-calculus (namely, \(\Lambda_{\infty}^{001}\)).

This short paper solves the question whether the converse property also holds: if the approximants of some term reduce to the approximants of another term, is there a β-reduction between these terms?

This happens to be true for the λ-calculus, as we show, but our proof fails in the infinitary case. We exhibit a counter-example, refuting the conservativity for \(\Lambda_{\infty}^{001}\).

R.C. et L. Vaux Auclair, Taylor Expansion Finitely Simulates Infinitary β-Reduction (en révision).

Soumis à Logical Methods in Computer Science. Titre provisoire.

RésuméPDFarXiv

Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of λ-terms has been broadly used as a tool to approximate the terms of several variants of the λ-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. This led us to consider extending this formalism to the infinitary λ-calculus, since the \(\Lambda_{\infty}^{001}\) version of this calculus has Böhm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem.

We give a (co-)inductive presentation of \(\Lambda_{\infty}^{001}\). We define a Taylor expansion on this calculus, and state that the infinitary β-reduction can be simulated through this Taylor expansion. The target language is the usual resource calculus, and in particular the resource reduction remains finite, confluent and terminating. Finally, we state the generalised Commutation theorem and use our results to provide simple proofs of some normalisation and confluence properties in the infinitary λ-calculus.

R.C., Développement de Taylor et λ-calcul infinitaire (2020).

Mémoire de recherche dans le cadre d'un M2 d'informatique. Sous la direction de L. Vaux Auclair.

R.C., Equivalence of Three Categorical Notions of Model for Dependent Types (2017).

Mémoire de recherche dans le cadre d'un M1 d'informatique. Sous la direction de T. Streicher.

Exposés

Talks

Je suis toujours ravi de présenter ce que je fais, n'hésitez pas à me contacter !

I'm always glad when I can present what I do, feel free to contact me!

2023

How To Play The Accordion. On the (Non-)Conservativity of the Reduction Induced by the Taylor Approximation of λ-Terms, TLLA 2023 (Rome), 1 juil. 2023. PDF.

Category theory stories 3: Where \( P \wedge (Q_1 \vee Q_2) \Leftrightarrow (P \wedge Q_1) \vee (P \wedge Q_2) \), PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), 20 avr. 2023. Exposé introductif sur les adjonctions.

La réduction du λ-calcul à ressources induit une extension conservative de la β-réduction des λ-termes, Séminaire Logique & Interactions (I2M, Marseille), 2 mars 2023.

Taylor Expansion for the Infinitary λ-Calculus, Journées du groupe de travail SCALP SCALP Working Group Days (CIRM, Marseille), 16 févr. 2023. Diapos.

Taylor Expansion as a Finitary Approximation Framework for the Infinitary λ-Calculus, école d'hiver «  Les mathématiques discrètes et la logique : des mathématiques à l'informatique » “Discrete mathematics and logic: Between mathematics and computer science” winter school (CIRM, Marseille), 18 janv. 2023. PDF.

Taylor expansion for the infinitary λ-calculus, Séminaire PPS (IRIF, Paris), 12 janv. 2023. Diapos.

Des preuves qui calculent, Journée des doctorant⋅es de l'ED 184 (Marseille), 11 janv. 2023.

2022

Category theory stories 2: Where a real number is nonnegative whenever it is greater than all negative numbers, PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), 8 déc. 2022. Exposé introductif sur le lemme de Yoneda.

Category theory stories 1: Where we'll discover proofs by induction, PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), 17 nov. 2022. Exposé introductif autour des F-algèbres initiales.

Calculs impossibles et calculs difficiles, PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), 19 mai 2022. Deux exposés introductifs sur les machines de Turing et la calculabilité. Diapos.

De toute façon les maths c'est que du calcul, PhD student's seminar Séminaire des doctorant⋅es (I2M, Marseille), 4 mai 2022. Exposé introductif sur la correspondance de Curry-Howard.

Taylor Expansion for the Infinitary λ-Calculus, Journées nationales du GdR IM (CNRS, Lille), 1 avr. 2022. PDF.

2021

Comment développer une preuve en série entière (ou presque), PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), 2 déc. 2021.

Développement de Taylor en λ-calcul infinitaire, Séminaire Logique & Interactions (I2M, Marseille), 25 nov. 2021. Deux exposés.

Calcul et Raisonnement sont dans un bateau, Journée de rentrée du M1 MAAP (Marseille), 3 sept. 2021.

Lambda-calcul et correspondance de Curry-Howard, PhD student's seminar Séminaire des doctorant⋅es (I2M, Marseille), 16 mars 2021.

Sciences sociales Social sciences

Dans une autre vie, j'ai suivi une formation en sciences sociales et je me suis en particulier intéressé à la définition et la transmission de savoirs pratiques par les enseignements des mathématiques, ainsi qu'aux filières « d'élite » de l'enseignement supérieur, à leur accès et au contenu de leur formation. J'ai creusé ces interrogations en travaillant sur les colles de mathématiques en CPGE sous la direction d'Emmanuelle Picard.

In a previous life I studied social sciences, and took a particular interest in the definition and the transmission of practical knowledge through the teaching of mathematics, as well as in the “elite” branches of higher education, in the access to these and in the content of their eudcational programs. I delved into this subject by studying a system of oral tests (the colles) in the French classes préparatoires, under the supervision of Emmanuelle Picard.

Travaux

Published work

R.C., Pêcher des poissons pour leur apprendre à nager ? II. En « colles », les mathématiques au service d'une formation élitiste (à paraître).

In P.-M. Menger, P. Verschueren (dir.), Le Monde des mathématiciens (actes du colloque « Mathématiques, communautés et institutions », Collège de France, 2020), éd. du Seuil, à paraître à l'automne 2023.

RésuméPDF

L'importance persistante des mathématiques dans l'accès à une grande part des filières d'élite en France pousse à s'interroger sur le rôle concret joué par cette discipline et ses cadres d'enseignement dans la (re)production d'une « jeunesse dominante ». Étudiant dans trois lycées prestigieux les « colles » de mathématiques, interrogations orales au cœur du dispositif pédagogique des classes préparatoires, nous montrons que l'apprentissage et l'évaluation des savoirs y sont le support d'une prise en charge institutionnelle des élèves (au moins autant que l'inverse) visant à leur transmettre des dispositions qui excèdent largement le seul cadre des mathématiques. La structure des jugements mathématiques des interrogateurs fait apparaître une valeur d'autonomie, nourrie de la dualité rigueur/intuition classique en mathématiques, qui renouvelle l'idéologie du don bourdieusienne et interfère avec le passé social des élèves — au risque d'agir en différenciant leurs trajectoires.

R.C., Coller en mathématiques. Rite disciplinaire et formation des élites (2019).

Mémoire de recherche dans le cadre d'un M1 de sciences sociales. Sous la direction d'E. Picard.

Enseignement Teaching

À l'Université d'Aix-Marseille

At Aix-Marseille University

Je suis chargé d'enseignement à la Faculté des sciences d'Aix-Marseille Université, au sein des départements de mathématiques et d'informatique.

I teach in the mathematics and computer science departments of Aix-Marseille University's Faculty of Sciences.

Cette année, je donne un cours « Langage mathématique » en L1 (avec L. Vaux Auclair), des TD de calculabilité en L3 (pour K. Perrot) et des TP de structures de données discrètes en L2 (pour A. Milani). Précédemment, j'ai donné un cours d'analyse en L1, des TD d'analyse et d'introduction au formalisme mathématique en L1, des TP d'introduction à la programmation en L1, des TD et TP de bases de données en L3.

This year, I teach a “Mathematical language and Reasoning” course (1st year bachelor, with L. Vaux Auclair) and I give tutorials in Calculability (3rd year bachelor, for K. Perrot) and labs in Discrete data structures (2nd year bachelor, for A. Milani). Previously, I gave a course in Calculus (1st year), tutorials in Calculus (1st year) and Databases (3rd year), and labs in Programming (1st year).

Détail : Details: 22-23 ⋅ 21-22 ⋅ 20-21

Auparavant

Before

Pendant deux ans, j'ai donné des interrogations orales en classes préparatoires (MPSI, BCPST et khâgne B/L).

During two years, I gave weekly oral exams in classes préparatoires (MPSI, BCPST and khâgne B/L).

Il y a quelques années, j'ai co-organisé un groupe de travail étudiant de théorie des catégories (avec Meven Bertrand). On a des super notes de cours qu'on met au propre très lentement et qui seront en ligne, un jour.

A few years ago, I co-organised a category theory working group for fellow students (with Meven Bertrand). We wrote great notes that we are slowly cleaning up and that will be online, one day.

D'autres choses Other stuff

Quelques liens

A few links

Le séminaire des doctorant⋅es de l'I2M (et du CPT) à Luminy, que j'ai eu la chance de co-organiser jusqu'en 2022, est un chouette endroit que je recommande à tou⋅tes les thésard⋅es en maths, physique et info à Marseille.

The I2M (and CPT) PhD student's seminar in Luminy, that I had the chance to co-organize until 2022, is a nice place — I recommend it to any PhD students in maths, physics or CS in Marseille.

Partant du constat que le monde académique contribue bien au-delà du « nécessaire » au dérèglement climatique, le manifeste Theoretical Computer Scientists For Future défend une plus grande prise en compte des enjeux écologiques à toutes les échelles de l'activité de recherche (en l'occurrence, dans ma discipline).

In response to the observation that the academia contributes to the climate change far more than “necessary”, the Theoretical Computer Scientists For Future manifesto advocates for taking greater account of the ecological implications of the research activities, at all scales (and in this case in my academic field).

Du code

Some code

Ce site est construit avec un modèle maison en PHP, qui a pour principaux (et uniques) mérites d'automatiser une mise en page minimaliste, de gérer le multilinguisme et d'afficher de jolies (?) listes de publications. Je l'ai mis en ligne pour des copains, il est à la disposition de qui veut s'en servir.

This website is built with a homemade PHP template, the main (and only) merits of which are to automate a minimalist layout, to handle multiple languages and to render nice (?) lists of publications. I made it available for some friends, it can be used by anyone who wants to.

Contact

I2M, site de Luminy Luminy site
Bâtiment Building Ancienne BU, bureau office A206
163 avenue de Luminy, case 907
13288 Marseille Cedex 9

Tel. (+33) 4 91 26 95 91

Courriel : Email: remy point dot cerda chez at univ-amu.fr .
Voici ma clef publique. Here is my public key.

J'ai cru par l'esprit
me libérer de mes prisons
Mais l'esprit lui-même est une prison
J'ai essayé d'en repousser les parois
J'essaie toujours

— Abdellatif Laâbi