Welcome to my homepage! I am a researcher in theoretical computer science at École normale supérieure de Lyon, Plume team, on an individual postdoctoral fellowship from LabEx MILyon (supervised by Denis Kuperberg).
Previous positions & job applications (click-to-expand using the HTML5
- In 2024, I’m applying to CNRS – here’s a detailed summary of previous work and research statement, both in French – and to Inria, whose “dossier de candidature” fits in a single file.
- Here’s my (very slightly updated) submitted research project in French for the LabEx MILyon postdoc grant.
- March to August 2022: postdoc on Noam Zeilberger’s LambdaComb grant, at École Polytechnique / Inria Saclay.
- September 2021 to February 2022: research engineer in the SPICY team in IRISA (Rennes, France), cf. below
- September 2018 to August 2021: PhD student at Université Paris XIII (which uses the brand “Sorbonne Paris Nord” despite having no connection at all to the historical Sorbonne); see below for my dissertation. I’m technically a student of a student of (Corrado Böhm|Jean-Yves Girard) but concretely, most of my collaborations during my PhD were with people outside of my lab (mainly Cécilia Pradic).
Contact / personal information
|Lê Thành Dũng
nltd at nguyentito dot eu
|@firstname.lastname@example.org (Mastodon) | CS Theory StackExchange | ORCID
|photo (taken by Lwenn Bussière-Caraes)
Actually important stuff
The overriding concern of our age is the ongoing environmental disaster. There is a Pledge for sustainable research in theoretical computer science that you can sign if you work in that field, and one of its creators, my colleague Antoine Amarilli, has a lovely list of actions and commitments that he takes out of concern for the climate crisis; personally, I am a vegetarian and I haven’t boarded a plane since summer 2019 (while managing to visit Warsaw twice since then). I am also in favor of remote attendance options in scientific conferences (preferably not using proprietary software such as Zoom but it would still be a lesser evil compared to forcing people to burn kerosene).
All my publications until now are open access. I refuse to submit my work to any venue that does not meet this requirement (being allowed to upload a preprint is not sufficient), no matter how prestigious it may be – anyway, publications should be judged on their own merits. (I’ve been pressured to do so before, and was relieved that the paper was rejected.) I also pledge not to provide peer review for closed-access venues. Even though many people will try to convince you otherwise, I do not believe the above commitments have significantly impaired my chances of obtaining a permanent academic position (if I want to despite the sad state of higher education and research in France…).
The issues raised by the Just Mathematics Collective – social justice and the ethical implications of our work – are also of the utmost importance. See what Grothendieck thought of scientific research in 1972 (in French).
My research used to focus on connections between linear logic, a logical system born out of the proofs-as-programs correspondence (“Curry-Howard isomorphism”), and other topics in theoretical computer science such as graph theory, computational complexity, formal languages… Nowadays I also invest much of my working time in this latter field — more precisely, finite automata / transducers / semigroups. I also enjoy categorical perspectives and approaches to all of the above; those are well-established applications of category theory, but not the trendy kind of “applied category theory”. (I’ve been teaching the basics of category theory to students at ÉNS Lyon.)
Outside of my research, I also have other scientific interests which I lack the time to pursue (click to expand)
- Algorithms, especially complexity theory and combinatorial optimization (I have a master’s degree in Operations Research); in a past life, I also designed a few programming contest problems
- Other areas involving proofs-as-programs: functional programming languages (my research interests began by learning Haskell), proof assistants, philosophy of mathematics (see the Girard fanclub known as “Réflexions sur les fondements de la logique (ReFL)”, for whom I gave a talk in French about categorical semantics of λ-calculi), …
- Classical mathematics (e.g. algebra / topology / categories, but also real analysis, convex optimization, …)
- At some point in the future I’d like to learn Rust and do some systems programming for fun (e.g. the protohackers challenges); or perhaps dabble in infosec.
The expository text below does not exhaustively list my publications, but all long versions of my papers can be found on arXiv or HAL. You can also go check out Cécilia Pradic’s website for our joint papers, some of which also have the fictional coauthor Camille Noûs.
Current research themes
Transducers (in particular (poly)regular functions)
Slides: Algebraic recognition of regular functions (alternate slides+video for category theorists on the SYCO 11 webpage); Comparison-free polyregular functions a.k.a. “polyblind functions”; Transducers beyond linear growth: old and new; Two-way automata and transducers with planar behaviours are aperiodic (warning: mostly correct but not 100%)
Automata theory starts with the well-known correspondence between regular languages and various kinds of finite-state automata. What happens if you consider automata-like devices that, instead of recognizing languages, compute string-to-string (or tree-to-tree) functions? Such devices are called transducers. Interestingly, there is a plethora of transducer models, sometimes but not always equally expressive.
In particular, the class of regular string functions admits several equivalent definitions by machine models (two-way transducers, copyless streaming string transducers, …), and another one using logic (MSO transductions), attesting to its robustness/canonicity. Mikołaj Bojańczyk and I have proposed a concise algebraic characterization of regular functions, analogous to recognizability by finite monoids for regular languages, but using a little bit of category theory.
A more recent trending topic in string transducers is polyregular functions. They were given this name by Mikołaj because their output has size polynomially bounded in the input size, and they extend the regular functions (which have linear output size). Cécilia Pradic, Sandra Kiefer and I have a submitted preprint with two different proofs that “nesting” two regular functions does not suffice to define all polyregular functions with quadratic output size. By the way, this refutes (twice) the central claim of a LICS 2020 paper; what does that say about prestigious conferences in theoretical computer science…
I have also been fortunate to interact with several other talented researchers in transducer theory, such as Gaëtan Douéneau-Tabot (whose thesis further studies polyblind functions, among many other impressive results) and Nathan Lhote (with whom I have an ongoing project).
Automata vs λ-calculus, or LAMBDA: the ultimate finite-state device
Cécilia Pradic and I have a research programme that we call “Implicit automata in typed λ-calculi”. Implicit computational complexity seeks to characterize complexity classes by using constrained programming languages; we are investigating a counterpart for automata and transducers, relying on linear/affine type systems. This includes a characterization of regular functions, and has led us to revisit automata-theoretic construtions in a categorical framework. Most of this is covered in my PhD dissertation (final revision: March 2023; local copy; slides of the defense in French). I’ve been surprised and elated to see that our work has even been mentioned in a talk by Gordon Plotkin!
In an upcoming paper, that has been “in preparation” for a year now (shame on me…), I will characterize the “non-uniformly definable functions” from trees to tress in the simply typed λ-calculus. The abstract of my talk at the Dagstuhl Seminar on Regular Transformations covers some related topics concerning higher-order phenomena in transducers.
It seems that a connection between MSO tree transductions and linear λ-calculus was first suggested by Kanazawa in a 2008 talk without proof; the same statement (up to insignificant details) was later proved by Gallot, Lemay and Salvati. With Gabriele Vanoni, we are working on revisiting this “higher-order transducer” take on the topic using tools derived from the “geometry of interaction”. Morally, all this is closely related to the aforementioned implicit characterization of regular functions.
More recently, I have become interested in Sylvain Salvati’s regular languages of simply typed λ-terms at arbitrary types. Vincent Moreau and I have a paper out about their various equivalent definitions (see also Vincent’s slides).
Complexity of convertibility/normalization for λ-calculi
In this preprint (associated slides) I clarify the (little-)known fact that β-convertibility for simply typed λ-terms is TOWER-complete, and extend this result to safe λ-terms. My TOWER-hardness proof for the safe case is quite different than the previous approach for simply typed λ-terms, and is grounded in connections with automata. It would be nice to extend the membership in TOWER to sum types, cf. this TCS.SE question.
With Anupam Das, Damiano Mazza and Noam Zeilberger, we have a tentative proof that the convertibility of planar λ-terms is P-complete. This is our second attempt, after a previous one turned out to be subtly wrong, and it has not been peer-reviewed, so beware…
Formal methods for security
I spent 5 months as a research engineer writing OCaml code for a proof assistant called Squirrel, whose logic is tailored to verifying security properties of cryptographic protocols.
Combinatorics of proof nets
Slides: A complexity gap between pomset logic and system BV (invited talk); Proof nets through the lens of graph theory (includes some unpublished observations on cyclic MLL); Coherent interaction graphs
The study of linear logics has led to developing formal proof systems going beyond the limits of the traditional sequent calculus. Deep inference liberalizes the possible applications of deduction rules. Proof nets represent proofs as graph-like objects from which it is not obvious to reconstruct a sequence of deductions; subtle combinatorial conditions are needed to ensure that a proof net is correct.
The first logic to use deep inference, Alessio Guglielmi’s system BV, attempted to be an equivalent presentation of an existing logic based on proof nets, namely Christian Retoré’s pomset logic. But in fact, these two logics are not equivalent; this is what Lutz Straßburger and I showed in a journal paper. We hope this paper will also serve as a useful reference for BV and pomset logic; indeed, while I don’t work on this topic anymore, it is still active (people have extended BV to directed graphs as generalized formulas and found connections with higher-order causal processes).
With Thomas Seiller, we also built a “geometry of interaction” model of MLL which gives a computational/interactive explanation of a correctness criterion for proof nets in Multiplicative Linear Logic by Christian Retoré (again!) based on cographs. Erratum (thanks to Valentin Maestracci): the proof of Proposition 37 contains a mistake (therefore, the internal completeness claim is wrong). We later realized that this could be extended to pomset logic (see the end of these slides). A throwaway sentence in the conclusion mentioning possible uses of prime graphs and modular decomposition in proof theory coincidentally anticipated a line of work that appeared soon afterwards by Matteo Acclavio and his collaborators.
Finally, in another arXiv note, I prove some purely graph-theoretic minor results initially motivated by my early work on proof nets. In particular, this concerns perfect matchings, edge-colored graphs and paths/trails avoiding forbidden transitions.
Related: unfruitful work in combinatorial optimization (Master’s internship)In 2016, I did a 4-month internship with Christoph Dürr and Nguyễn Kim Thắng for my master’s degree. We tried to design an approximation algorithm for the online node-weighted Steiner forest problem. Our approach didn’t work, but we improved our understanding of the difficulty of the problem. However, thanks to a recreational algorithmic puzzle given by Christoph during this internship, I learned about the relationship between perfect matchings and edge-colored graphs, which would eventually lead to my above-mentioned work. You can see my first ideas on these topics and their connection to linear logic in the slides of the defense (in French).
(Unfinished) Denotational semantics of polymorphism vs space complexity
What led me to implicit automata (cf. above) was finding out that regular languages occur in a language with linear types designed for implicit complexity, giving an unexpected answer to a question by Patrick Baillot. It turns out that the proof for this relies on old ideas on the denotational semantics of second-order linear logic. Another direction was to understand how to go beyond regular languages using the same ideas.
The result was an implicit characterization of something between L and NL (probably L…), whose proof uses a bit of semantics and of category theory (in particular normal functors). The implicit complexity side of the story – a joint work with my long-term collaborator Cécilia Pradic – was published. The semantics side is far from being as rigorous as I would like and is projected to be rewritten at some point (I don’t have the excuse of having to write my PhD dissertation anymore…); in the meantime, you can take a look at this old preprint.
Involvement in computer science teaching / outreach
Vulgarisation scientifique (science popularization in French)
I was in charge of the semifinals problems in 2015 and 2016. Furthermore, in 2015, I was the main developer on the game for which the contestants had to write an AI during the finals; and from mid-2015 to mid-2016, I was heavily involved in the logistics of both Prologin and Girls Can Code! as a board member.
From 2017 to 2018, I designed and implemented programming contest exercises as a freelance consultant for Isograd, selling the skills that I had developed thanks to Prologin to the private sector.
Disclaimer: I was always terribly slow at this stuff, compared to the people who perform well in actually difficult contests such as ICPC, Codeforces, etc.
In Fall 2023 I’ll be teaching a modest introduction to category theory for computer scientists at ÉNS Lyon for 5 weeks!
In September 2023 I taught a 1-week intensive course (6h/day) on regular expressions and finite automata to 2nd year students at a private sector engineering school (EPITA Lyon).
In the 2021-2022 academic year I worked as a teaching assistant in Université Rennes 1. I taught NoSQL databases in the first semester, and deductive program verification (for undergrads, there’s even a published paper on this course) in the second semester.
From 2018 to 2021, I was a TA at Institut Galilée as part of my PhD, on topics such as hardware architecture, Unix system calls, algorithms and data structures, parallel random-access machines and λ-calculus, functional programming with OCaml, and XML technologies.
In 2016, I gave tutorial sessions for the Algorithms course given by Gaël Mahé at Université Paris 5 Descartes (now merged into Université Paris Cité) for second-year students.