Tito's presence on the Web Neurodiversity

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). (And here’s my (very slightly updated) submitted research project in French.)

Previous positions (click-to-expand using the HTML5 <details> element)

Contact / personal information

Family name: Nguyễn
Given name: Lê Thành Dũng
E-mail address: nltd at nguyentito dot eu
Social media: @tito@sciences.re (Mastodon) | CS Theory StackExchange | ORCID
Visual identification: 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).

Research

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”.

Outside of my research, I also have other scientific interests which I lack the time to pursue:

I tend to agree with David Madore when he says that “the only people interested in publication lists look like they to want to count them, not to read them” (translation mine). Nevertheless, for an exhaustive list (with obsolete preprints and miscellaneous arXiv notes), you can find my dblp profile here. (It has a missing tilde on my family name – this spelling issue also occurs on arXiv due to lack of Unicode support.) The expository paragraphs below are not guaranteed to contain links to all my papers.

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…

Cécilia and I have a couple other papers on (poly)regular functions (including one inspired by Peter Hines), with the fictional coauthor Camille Noûs; again, go check out Cécilia’s website! I have also been fortunate to interact with several other talented researchers in transducer theory, such as Gaëtan Douéneau-Tabot (who further studied polyblind functions) and Nathan Lhote (with whom I have an ongoing project).

Automata vs λ-calculus, or LAMBDA: the ultimate finite-state device

Slides: Aperiodicity in a non-commutative logic; Implicit automata in typed λ-calculi; A transducer model for simply typed λ-definability; Geometry of interaction meets actually existing automata

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 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 single-authored paper, that has been “in preparation” for a year now (shame on me…), I solve Conjecture 1.4.3 of my dissertation on the “non-uniformly definable functions” in the simply typed λ-calculus; this has been the subject of blackboard talks in seminars. The abstract (soon to be online) of my talk at the Dagstuhl Seminar on Regular Transformations covers some related topics concerning higher-order phenomena in transducers.

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 preprint out about their various equivalent definitions.

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…

Older work

Combinatorics of proof nets

Slides: Proofs nets through the lens of graph theory (includes some unpublished observations on cyclic MLL); A complexity gap between pomset logic and system BV; 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. 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

Slides: Hypercoherences as games for space-efficient iterations?

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)

Un peu de publicité (en français) sur l’usage des monades en programmation, qui évoque rapidement la sémantique catégorique à la fin. (Si vous avez aimé ça, vous pouvez booster ce post sur Mastodon.)

En 2015, Jérémy Ledent et moi avons écrit des articles pour Tangente, un magazine de maths pour lycéens, sur la correspondance preuves-programmes et sur la théorie homotopique des types.

Competitive programming

As a member of the Prologin organization from 2014 to 2018, I helped organize Prologin, a programming contest for people under 20 years old, and Girls Can Code!, a summer coding camp.

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.

University teaching

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.