Hi, I'm Cécilia! I have been a lecturer at Swansea University since fall 2021; this page is essentially a list of papers/drafts I have been involved with, most of those should be freely available on arxiv or HAL if you need them. I also have some of the slides I've been using in talks. If you are a student looking for teaching-related material I might have mentioned, probably you want to scroll down at the end of the page.
I am generally interested in topics around logic, realizability, automata theory and type theory. Before that, I was a doctoral student at ENS Lyon and at the University of Warsaw, under the supervision of Colin Riba and Henryk Michalewski, and went on to be a postdoc for two years at the university of Oxford, working with Michael Benedikt. My thesis focused on some of the constructive aspects of Monadic Second Order logic.
Synthesizing nested relational queries from implicit
specifications: via model theory and via proof theory, with Michael
Benedikt and Christoph Wernhard, LMCS 2024, arxiv
On the Weihrauch degree of the additive Ramsey theorem, with
Arno Pauly and Giovanni Soldà, Computability 2024, arxiv
Synthesizing Nested Relational Queries from Implicit
Specifications, with Michael Benedikt and Christoph Wernhard, PODS
2023, arxiv
On the Weihrauch degree of the additive Ramsey theorem over the
rationals, with Giovanni Soldà, CiE 2022, pdf
Comparison-free polyregular functions, with Lê Thành Dũng
Nguyễn and Camille Noûs, ICALP 2021, pdf
Generating collection queries from proofs, with Michael
Benedikt, POPL 2021, arxiv
Implicit automata in typed λ-calculi I: aperiodicity in a
non-commutative logic, with Lê Thành Dũng Nguyễn, ICALP 2020, pdf
From normal functors to logarithmic space queries, with Lê
Thành Dũng Nguyễn, ICALP 2019, pdf
Kleene Algebra with Hypotheses, with Amina Doumane, Denis
Kuperberg and Damien Pous, FOSSACS 2019, pdf
A Dialectica-Like Interpretation of a Linear MSO on Infinite
Words, with Colin Riba, FOSSACS 2019, pdf
LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear
Logic, with Colin Riba, LICS 2018, pdf
A Curry-Howard Approach to Church's Synthesis, with Colin Riba,
FSCD 2017/LMCS 2019, arxiv
The Logical Strength of Büchi’s Decidability Theorem, with
Leszek Aleksander Kołodziejczyk, Henryk Michalewski and Michał
Skrzypczak, CSL 2016/LMCS 2019, arxiv
Integrating Linear and Dependent Types, with Nick Benton and
Neel Krishnaswami, POPL 2015, pdf source code
Olivia Weston (MRes defended in 2024)
Ian Price (PhD,
current)
Implicit automata in λ-calculi III: affine planar
string-to-string functions, with Ian Price, submitted arxiv
Two-way automata and transducers with planar behaviours are
aperiodic, with Lê Thành Dũng Nguyễn and Camille Noûs, submitted arxiv
Refutations of pebble minimization via output languages, with
Sandra Kiefer and Lê Thành Dũng Nguyễn, submitted arxiv
Implicit automata in typed λ-calculi II: streaming transducers vs
categorical semantics, with Lê Thành Dũng Nguyễn and Camille Noûs,
pdf
Cantor-Bernstein implies Excluded Middle, with Chad E. Brown,
arxiv formalization in Coq
Dumped here.
I don't do much of that these days, but I did spend some time with computers and proof assistants in my life.
I was motivated by a nice IRC discussion to write a Haskell thingymagic of questionable utility that actually runs. It prints out symbols like { ω + -ω, { η · ω, -ω }η }η generated by some DFAs and that is enough to make me smile.
Below are some past or current teaching material. If you are currently enrolled in a module in Swansea, all you need should already be hosted on canvas.
c.lastname@swansea.ac.uk or ceclastname@gmail.com