I am a researcher in theoretical computer science, currently a postdoc at École normale supérieure de Lyon, Plume team; I will probably join CNRS on a permanent position in a few months (see below for my job application materials). My research interests are in “logic in computer science”: λ-calculus, automata theory, and connections between these two topics.

Sometimes, I teach computer science (not just theory!) in universities. In a former life, with more free time and energy available, I also used to enjoy writing programs that can run on actual computers, science popularization, and pure mathematics (see my page about old stuff in French).

E-mail address:
nltd@nguyentito.eu
Social media: Mastodon | CS Theory StackExchange | ORCID
Visual identification: photo (86KB) taken at ÉNS Lyon
(+ higher-res photo (3.7MB) by Lwenn Bussière-Caraes)
Previous positions and job applications (click-to-expand using <details>)

I support:

TCS4F

Theoretical Computer Scientists for Future — see also Antoine Amarilli's list of actions and commitments 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.) Environmental responsibility is a good reason — accessibility is another one — in favor of remote attendance options in scientific conferences.

NFVNR

No free view? No review!, a pledge to boycott reviewing work for journals or conference proceedings which are closed access, or which charge unfair prices to authors. I also refuse to publish in such venues, no matter how prestigious they might be; anyway, publications should be judged on their own merits.

I also find this stuff worth paying attention to:

Teaching

In Fall 2023 I taught a modest introduction to category theory for computer scientists at ÉNS Lyon for 5 weeks. This course will be proposed again in Fall 2024.

In September 2023 I taught a 1-week intensive course (6h/day) on regular expressions and finite automata (with Python implementations) to 2nd year students at a private sector engineering school (EPITA Lyon). Yes, that is a politically questionable choice!

During my PhD, I served as a teaching assistant at Institut Galilée on topics such as hardware architecture, Unix system calls, algorithms and data structures, functional programming with OCaml, and XML technologies. I have also worked as a TA in some other places; in particular, for a deductive program verification course for undergrads at Université Rennes 1 (there's even a published paper on this course).

Research

My research used to focus on linear logic, a logical system born out of the proofs-as-programs correspondence (“Curry-Howard isomorphism”) — roughly speaking, a linear function/implication can only “use its argument/assumption once” — and its connections with other topics such as graph theory, computational complexity, formal languages… Nowadays I also invest much of my working time in this latter field, more precisely on transducers: variants of finite-state automata with output. 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”.

The process that led to one of my major results, “pomset logic ≠ system BV”, started from discovering a wrong lemma in a peer-reviewed paper from 1997. One of my works on transducers actually refutes (twice) the central claim of a LICS 2020 paperLICS is among the most prestigious conferences in its field (and its proceedings are sadly closed access). While some of my colleagues in type theory develop formal proof assistants to make mathematical results more reliable, I am more interested in errors and corrections in the scientific literature as a social matter; Enka Blanchard and I presented some banal thoughts on the subject (slides) at the Undone Computer Science 2024 workshop.

Erratum on Coherent interaction graphs (N. & Seiller, Linearity–TLLA 2018) The proof of Proposition 37 contains a mistake; therefore, the internal completeness claim might be wrong. (Thanks to Valentin Maestracci for finding the bug.)

My coauthors: mainly Cécilia Pradic and the fictional Camille Noûs, as well as Mikołaj Bojańczyk, Anupam Das, Sandra Kiefer, Damiano Mazza, Vincent Moreau, Thomas Seiller, Rafał Stefański, Lutz Straßburger, Gabriele Vanoni, Noam Zeilberger. In preparation: Abhishek De, Paul Gallot, Charles Grellois, Nathan Lhote.

Major research themes (click to expand):

Transducers (polyregular functions, macro tree transducers, …)

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.

The class of regular string functions has several equivalent definitions by machine models (two-way finite transducers, copyless streaming string transducers, …), and another one using logic (MSO transductions), attesting to its robustness/canonicity.

Polyregular functions are a more recent trending topic in string transducers. They were given this name by Bojańczyk because their output has size polynomially bounded in the input size, and they extend the regular functions (which have linear output size).

Implicit automata in typed λ-calculi (including my PhD thesis) (or LAMBDA: the ultimate finite-state device)
Slides: Implicit automata in typed λ-calculi (variant with some different material); Geometry of interaction meets actually existing automata

The field of implicit computational complexity seeks to characterize complexity classes by using constrained programming languages. Linear type systems are typically used for that purpose, since they enable static restrictions on duplication and iteration. Cécilia Pradic and I have been investigating a counterpart to implicit complexity for automata and transducers; it turns out “single-use” or “copyless” restrictions, that look a lot like linearity, already played an important role in automata theory. Our starting point was a theorem of Hillebrand & Kanellakis about characterizing regular languages in the simply typed λ-calculus.

This is the topic of my PhD dissertation (final revision: March 2023; local copy; slides of the defense (December 2021)). For a shorter read, you can look at the first paper in the series: Aperiodicity in a non-commutative logic (perhaps my favorite result in my entire career).

There is more to say about this ongoing research programme: it is closely related to earlier works concerning higher-order transducers (though our characterization of polyblind functions cannot be expressed in this framework) and abstract categorial grammars; ideas from higher-order model checking can be used to handle infinite trees; …

Previously: Combinatorics of proof nets (pomset logic & MLL+Mix) Slides: Proof nets through the lens of graph theory (contains remarks not published elsewhere); A complexity gap between pomset logic and system BV

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, system BV, attempted to be an equivalent presentation of an existing logic based on proof nets, namely pomset logic. But in fact, these two logics are not equivalent; furthermore, provability is more computationally difficult in pomset logic (it is Σ2P-complete) than in BV (NP-complete). This is what Lutz Straßburger and I showed in a journal paper, which hope 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; for instance, connections between pomset logic and higher-order causal processes have been found recently.

One important aspect of the above work is to draw inspiration from the literature on graph algorithms to study the proof nets of pomset logic. In another arXiv note, I prove some anecdotal graph-theoretic results initially motivated by my early work on proof nets for Multiplicative Linear Logic with Mix (MLL+Mix). In particular, this concerns perfect matchings, edge-colored graphs and paths/trails avoiding forbidden transitions. My interest in these objects started with a recreational algorithmic puzzle given by Christoph Dürr during an internship supervised by him and by Nguyễn Kim Thắng (for a master's degree in operations research). The connection between perfect matchings and proof nets was first discovered by Christian Retoré, who is also the inventor of pomset logic.

Finally, with Thomas Seiller, we also built a semantics of MLL+Mix which gives a computational / interactive explanation of a correctness criterion for proof nets in MLL+Mix by 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.

Other works (all more or less inspired by implicit automata):

Automata over infinite alphabets (atoms / nominal sets)

I have worked with Bojańczyk and Stefański on using ideas from linear logic to relax the “single-use restriction” on functions between orbit-finite sets, leading to a category with function spaces (weak monoidal closure). This was inspired by an ongoing project with Eberhart and Pradic on extending implicit automata in linear logic to infinite alphabets.

Regular languages of simply typed λ-terms & logical relations Slides: introductory, for automata theorists; more detailed, for programming language theorists

The use of finitary semantics to study λ-terms, which plays an important role in my work on “implicit automata”, had also led Sylvain Salvati to define regular languages of simply typed λ-terms at arbitrary types. Vincent Moreau have a paper about their various equivalent definitions, using logical relation arguments. (We also have a cute example: among the third-order encodings of untyped λ-terms (as syntax trees with binders modulo α-renaming), the subset of linear terms is regular.)

Complexity of convertibility/normalization for λ-calculi Slides: Simply typed convertibility is TOWER-complete even for safe λ-terms

Consider the following decision problem, for some fixed variant of the λ-calculus: given two terms as input, are they convertible? Equivalently, if we work in a normalizing system, do they reduce to the same normal form?

I showed that this problem is P-complete for planar λ-terms (also known as “ordered” or “non-commutative” λ-terms; joint work with Das, Mazza and Zeilberger) and TOWER-complete for safe λ-terms. In other words, the planarity (resp. safety) condition does not decrease the computational complexity of the convertibility problem in the linear (resp. simply typed) λ-calculus. The proof techniques for both results are inspired by my work on implicit automata.

(old & 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 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.

Some recent events: