Je suis doctorant à 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 Marseille Mathematics Institute (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, which consists in 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, et j'ai fait un peu de sciences sociales sur des questions liées à l'enseignement des mathématiques.

Apart from that I teach mathematics and computer science, and I did a little social sciences around questions related to the teaching of mathematics.

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.

En outre :

In addition:

• Je participe 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.
• Je contribue à Wikipedia et StackExchange.
• I contribute to Wikipedia and StackExchange.
• J'utilise la notation de Krivine.
• I use the Krivine notation.

Travaux

(Un)Published work

Voici une liste de travaux publiés ou non. Je suis aussi sur vos plateformes préférées, comme DBLP ou ORCID.

Here is a list of my work, published or not. I'm also on your favourite platforms, like DBLP or ORCID.

R.C., Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi. A fanfiction on [KPSdV'13] (to appear).

Extended abstract accepted by FICS 2024.

AbstractPDFLong version

Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that α-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce “mixed” binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets \(\Lambda^{abc}\) of \(abc\)-infinitary λ-terms (for \(a,b,c \in \{0,1\}\)) and of capture-avoiding substitution on α-equivalence classes of such terms.

R.C. and L. Vaux Auclair, Finitary Simulation of Infinitary β-Reduction via Taylor Expansion, and Applications (2023).

Logical Methods in Computer Science, Vol. 19, no. 4, 10.46298/LMCS-19(4:34)2023.

AbstractPDFarXiv

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. and L. Vaux Auclair, How To Play The Accordion. On the (Non-)Conservativity of the Reduction Induced by the Taylor Approximation of λ-Terms (unpublished).

AbstractPDFarXiv

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., Développement de Taylor et λ-calcul infinitaire (2020).

Second year Master thesis in Computer science, as part of a research internship. Under the supervision of L. Vaux Auclair.

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

First year Master thesis in Computer science, as part of a research internship. Under the supervision of 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!

2024

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi. A fanfiction on [KPSdV'13], FICS 2024 (Naples), Feb 19, 2024. PDF, Slides.

2023

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi, Séminaire Logique & Interactions (I2M, Marseille), Nov 23, 2023.

Uniformity and the Taylor expansion of infinitary λ-terms, Groupe de travail Sémantique (IRIF, Paris), Nov 14, 2023. Slides.

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

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), Apr 20, 2023. Introductory talk about adjoint functors.

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

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

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), Jan 18, 2023. PDF.

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

Des preuves qui calculent, Journée des doctorant⋅es de l'ED 184 (Marseille), Jan 11, 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), Dec 8, 2022. Introductory talk about the Yoneda lemma.

Category theory stories 1: Where we'll discover proofs by induction, PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), Nov 17, 2022. Introductory talk about initial F-algebras.

Calculs impossibles et calculs difficiles, PhD student's seminar Séminaire des doctorant⋅es (I2M-CPT, Marseille), May 19, 2022. Two introductory talks about Turing machines and computability. Slides.

De toute façon les maths c'est que du calcul, PhD student's seminar Séminaire des doctorant⋅es (I2M, Marseille), May 4, 2022. Introductory talk about the Curry-Howard correspondence.

Taylor Expansion for the Infinitary λ-Calculus, Journées nationales du GdR IM (CNRS, Lille), Apr 1, 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), Dec 2, 2021.

Développement de Taylor en λ-calcul infinitaire, Séminaire Logique & Interactions (I2M, Marseille), Nov 25, 2021. Two talks.

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

Lambda-calcul et correspondance de Curry-Howard, PhD student's seminar Séminaire des doctorant⋅es (I2M, Marseille), Mar 16, 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.

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.

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 (2023).

In P.-M. Menger, P. Verschueren (dir.), Le Monde des mathématiques, éd. du Seuil (actes du colloque « Mathématiques, communautés et institutions », Collège de France, 2020).

AbstractPDFURL

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).

First year Master thesis in Social sciences. Under the supervision of E. Picard.

Enseignement Teaching

À l'Université d'Aix-Marseille

At Aix-Marseille University

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

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

Cette année je donne des cours de « Langage mathématique » en L1 (avec P. Dehornoy), d'Algèbre linéaire en L1, d'Algorithmique des graphes en L3 (avec H. Daudé), de Logique et Calculabilité en M1, ainsi que les travaux dirigés associés. Précédemment, j'ai donné un cours d'analyse en L1, des cours et TD d'analyse et d'introduction au formalisme mathématique en L1, des TP d'algorithmique en L1 et en L2, des TD et TP de bases de données en L3, des TD de calculabilité en L3.

This year, I teach courses on: “Mathematical language” (1st year bachelor, with P. Dehornoy), Linear algebra (1st year bachelor), Graph algorithmics (3rd year bachelor, with H. Daudé), Logics and Computability (1st year master), as well as the associated exercise sessions. Previously, I gave several courses and tutorials in Calculus (1st year), tutorials on Computability (3rd year) and Databases (3rd year), and labs in Programming (1st year) and Algorithmics (2nd year).

Détail : Details: 23-24 ⋅ 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

Le manifeste Theoretical Computer Scientists For Future défend une plus grande prise en compte des enjeux écologiques à toutes les échelles de notre activité de recherche. Avec de nombreux⋅es collègues, je me suis par ailleurs engagé à limiter le recours à l'avion dans mes déplacements professionnels. En pratique, je ne le prends jamais.

The Theoretical Computer Scientists For Future manifesto advocates for taking greater account of the ecological implications at all scales of our research activity. Along with many fellow scientists, I also committed myself to limit plane travelling for my professional trips. In practice, I never take the plane.

Les standards de publication en informatique produisent de la recherche mal écrite et nuisent aux interactions scientifiques. Il serait temps de grandir.

Publication standards in Computer science produce poorly written research and are detrimental to scientific interactions. It is high time we grow up.

Contact

I2M, site de Luminy Luminy site
Bâtiment Building TPR2, bureau office 222
163 avenue de Luminy, case 907
13288 Marseille Cedex 9

Courriel : Email: rcerda chez at math point dot cnrs point dot 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