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:
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., Taylor Approximation and Infinitary λ-Calculi (2024).
PhD thesis (pre-defense version).
Under the supervision of L. Vaux Auclair et L. Regnier.
R.C.,
Nominal Algebraic-Coalgebraic Data Types, with
Applications to Infinitary λ-Calculi. A fanfiction on
[KPSdV'13] (
to appear).
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).
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).
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
Taylor Approximation and Infinitary λ-Calculi,
Soutenance de thèse
PhD thesis defense (Marseille), Jun 10, 2024.
Slides. 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).
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.
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.