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@types.pl (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 (from personal experience, Praha→Paris and Lyon→Wrocław→Warszawa→Leipzig are completely doable by some combination of train and night bus). The issues raised by the Just Mathematics Collective – social justice and the ethical implications of our work – are also of the utmost importance.

I’m glad to see that virtual conferences have taken off (out of necessity), but worried by the widespread use of tools with serious privacy and security issues. As computer scientists, we should hold ourselves to a higher standard so that society at large can follow our example! (Update around 2 years after writing this: the reign of Zoom shows no signs of stopping, sadly.)

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.

At one point, my intention was not to apply for permanent academic positions after my PhD, in order to escape the distorted incentives of contemporary research and the countless annoyances that well-meaning people will put you through for the sake of “career optimization”. Nowadays, I’m open to somehow landing such a position if it does not involve compromising on the above points nor spending actual effort on specifically compensating for this rigid stance. If you’re a non-tenured researcher intending to stay in academia, following my example may or may not be career suicide (corollary: you should probably not collaborate with me, which is pretty sad, but blame the system; though I probably have a less toxic attitude towards meeting deadlines than other colleagues).

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, if you’re looking for a specific paper of mine, it should be hyperlinked in the middle of some relevant explanatory paragraph below. For bean-counting purposes, you will have to follow this link to an exhaustive PDF resume in French. (Also, my dblp profile is not too hard to find, though it has a missing tilde on my family name – this spelling issue also occurs on arXiv due to lack of Unicode support.)

Expository and/or not my own work

See also the section on science popularization (in French).

A note on arXiv about a simple theorem in discrete geometry / linear algebra. (To be updated with a much simpler proof by Dorian Nogneng.)

Some slides on the expressivity of the simply-typed λ-calculus:

Transducers beyond linear growth: old and new: seminar talk in Bruxelles, introducing (poly)regular functions and the composition hierarchy of macro tree transducers (with my own application of the latter to the former at the end). 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.

Current research themes

Note: some papers mentioned are coauthored with the fictional researcher Camille Noûs.

Implicit automata in typed λ-calculi (my PhD topic)

Slides: Aperiodicity in a non-commutative logic; Implicit automata in typed λ-calculi; A transducer model for simply typed λ-definability

Implicit computational complexity seeks to characterize complexity classes by using constrained programming languages. Cécilia Pradic and I have been exploring a counterpart for automata and transducers, relying on subsystems of linear logic. This has also led us to revisit automata-theoretic construtions in a categorical framework. I’ve been surprised and elated to see that our work has even been mentioned in a talk by Gordon Plotkin!

See my PhD dissertation (final revision: March 2023), titled Implicit automata in linear logic and categorical transducer theory, and the slides of the defense (in French); or Cécilia’s website for more papers on the topic. 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.

More recently, I have become interested in the topic of regular languages of simply typed λ-terms at arbitrary types, introduced by Sylvain Salvati. We’ve started exploring various equivalent definitions with Vincent Moreau and the order 3 case with Amina Doumane.

Transducers (in particular (poly)regular functions)

Slides: Algebraic recognition of regular functions (for category theorists); Polyregular functions: some recent developments = polyblind + growth; The planar geometry of first-order string transductions

Transducers are automata that do not merely recognize languages, but compute string-to-string (or tree-to-tree) functions.

As a byproduct of the research carried out in my PhD, Cécilia Pradic and I have introduced the class of polyblind functions; originally they were called the “comparison-free” subclass of Mikołaj Bojańczyk’s polyregular functions. Cécilia, Sandra Kiefer and I also have a draft relating the growth rate and resource consumption of general polyregular functions.

Meanwhile, Mikołaj and I have proposed an algebraic characterization of regular functions, analogous to recognizability by finite monoids for regular languages, but using a little bit of category theory. In an upcoming paper Cécilia and I will also show that the star-free languages and first-order regular functions are recognized by the planar two-way automata proposed by Peter Hines.

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

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 draws from 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; A complexity gap between pomset logic and system BV; Coherent interaction graphs

In a pioneering work whose significance has been underestimated in my opinion, Christian Retoré provided a translation from proof nets for multiplicative linear logic (MLL), a graphical representation of proofs, to graphs equipped with perfect matchings. This relates the combinatorially tricky theory of proof nets with a well-studied counterpart in mainstream graph theory. I strengthened and refined the correspondence between the two – the relationship is not bijective, but it turns out there are reductions in both directions preserving many structural properties – and derived a lot of consequences that had been overlooked. See my journal paper extending the work I presented at the FSCD 2018 conference.

More recently, Lutz Straßburger and I have looked at two closely related extensions of MLL, Retoré’s pomset logic and Guglielmi’s system BV (the original deep inference system), using the same tools. This has led us to refute the two-decades-old conjecture that pomset logic and BV are equivalent. We hope that the significantly extended journal version of our CSL 2022 paper will serve as a useful reference for these two systems. (While I don’t actively 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 an interactive explanation of a correctness criterion by Retoré 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.

At the end of these slides I explain why proof net correctness for cyclic MLL (a non-commutative logic) can be decided in linear time, using a criterion by Paul-André Melliès reformulated using combinatorial maps.

Finally, in another arXiv note, I prove some purely graph-theoretic minor results initially motivated by my work on proof nets. In particular, this concerns 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 Cécilia Pradic (again!) – 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

fIn Fall 2023 I’ll teach category theory for computer scientists at ENS Lyon for 4 weeks!

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.