FR | EN

Ma tête 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).

My face 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:

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] (à paraître).
Version courte acceptée pour communication à FICS 2024.
R.C. et 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.
RésuméPDFarXiv
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 (non publié).
RésuméPDFarXiv
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!

2024
Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi. A fanfiction on [KPSdV'13], FICS 2024 (Naples), 19 févr. 2024. PDF, Diapos.
2023
Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary λ-Calculi, Séminaire Logique & Interactions (I2M, Marseille), 23 nov. 2023.
Uniformity and the Taylor expansion of infinitary λ-terms, Groupe de travail Sémantique (IRIF, Paris), 14 nov. 2023. Diapos.
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, Diapos.
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.

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).
RésuméPDFLien
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 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-2422-2321-2220-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