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.
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.
Publications
Synthesizing Nested Relational Queries from Implicit Specifications, with Michael Benedikt and Christoph Wernhard, PODS 2023, pdf
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, pdf
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, pdf
The Logical Strength of Büchi's Decidability Theorem, with Leszek Aleksander Kołodziejczyk, Henryk Michalewski and Michał Skrzypczak, CSL 2016/LMCS 2019, pdf
Integrating Linear and Dependent Types, with Nick Benton and Neel Krishnaswami, POPL 2015, pdf source code
Preprints
Revisiting the growth of polyregular functions: output languages, weighted automata and unary inputs, with Sandra Kiefer and Lê Thành Dũng Nguyễn, (the last section is a very rough draft), pdf
On the Weihrauch degree of the additive Ramsey theorem, with Arno Pauly and Giovanni Soldà, submitted pdf
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, pdf formalization in Coq
Slides
Here are a couple slides from talks I have given: PhD defense (23/06/20), Implicit automata in λ-calculi (I) (24/06/20, Warsaw automata webinar),
Implicit definitions of nested collections (06/11/20, Birmingham theory webinar, 04/12/20 seminar of the LINKS team (Lille)),
Implicit automata in λ-calculi (II) (16/12/20, IRIF gt réalisabilité,
05/02/21, Journées LHC, 08/03/21, GdT plume, 28/06/21, Structure meets Power
workshop (abstract)), Logical complexity of MSO over countable linear orders (17/02/21,
Manchester logic seminar, 25/01/23 York),
Implicit automata in λ-calculi (I.5) (19/03/21, IRIF gt automate), Comparison-free
polyregular functions (ICALP21), Cantor-Bernstein implies Excluded Middle (27/05/22, CS/Maths research day Swansea)
Code
I don't do much of that these days, but I did spend some time with computers
and proof assistants in my life.
A thing about countable total orders
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.
Some things I formalized in Coq
Ramsey's theorem via H-well-foundedness
link
A formalization of Stefano Berardi and Silvia Steila's paper
An intuitionistic version of Ramsey's Theorem and its use in Program Termination,
exhibiting a theorem analogous to the infinite Ramsey theorem admitting a constructive proof.
The paper introduces the notion of H-well-foundedness for relations, generalizing well-foundedness.
Their main theorem state that this notion is stable under finite union, which leads them to a second
constructive proof of Podelski and Rybalchenko's Termination Theorem.
- An equational theory for Mealy machines link
A little combinator language for letter-to-letter transducers together with a complete equational theory.
This essentially come from the remark that all such transducers correspond to the class of functions between
streams including lifting of maps between alphabets and closed by composition and parametric guarded fixpoints.
This appeared in my PhD thesis and I thought it might be folklore.
Dan Ghica, George Kaye and David Sprunger have a better version of the theorem over
there where one does not require that
uniqueness of fixpoints in a dedicated axiom.
Teaching
TD FDI 2018/2019
c.lastname@swansea.ac.uk or ceclastname@gmail.com