Welcome to my homepage! I am a graduate student in theoretical computer science at the Laboratoire d’informatique de Paris Nord (LIPN). I started my PhD in 2018 under the supervision of Stefano Guerrini and Thomas Seiller.

Contact / personal information:

Family name | Given name | Email address | Curriculum vitae & publication list |
---|---|---|---|

Nguyễn | Lê Thành Dũng | `nltd at nguyentito dot eu` |
PDF in French (updated Oct 2019), ORCID, dblp |

My research focuses 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, finite automata and transducers…

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

- Algorithms, especially complexity theory and combinatorial optimization (I have a master’s degree in Operations Research); in a past life, I also designed programming contest problems as a volunteer for Prologin and as a freelance consultant for Isograd
- Other areas involving proofs-as-programs: functional programming languages, philosophy of mathematics, …
- Classical mathematics (e.g. algebra / topology / categories, but also real analysis, convex optimization, …)

# Research

The click-to-expand parts in this section use the HTML5 `<details>`

element, no JavaScript involved! (However, Markdown/pandoc adds `<p>`

tags…)

## Expository and/or not my own work

A note on arXiv about a simple theorem in discrete geometry / linear algebra.

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

- A brief introduction to the motivations behind my research: very short talk (10 minutes) on λ-definable functions and automata theory, at the TACL 2019 summer school
- On Hillebrand and Kanellakis’s work in implicit complexity (a great source of inspiration!), talk at a GdR IM working group meeting

## Implicit automata theory via substructural types

*Implicit computational complexity* seeks to characterize complexity classes by using constrained programming languages. I have been recently exploring a counterpart for *automata and transducers*, relying on subsystems of linear logic.

A “secret ingredient” is the use of *Böhm-Berarducci encodings* (often called “Church encodings”): they were already known to be closely related to automata, as explained in the expository talks in the previous section (see also: higher-order model checking). An old open question that I’m interested in is: what functions between Church-encoded strings can the simply typed λ-calculus express?

An exciting result recently obtained with Pierre Pradic is a characterization of star-free languages and aperiodic regular functions using a *non-commutative* type system. More details to come!

## Talks

## Denotational semantics vs space complexity

What led me to implicit automata theory (cf. above) was finding out that regular languages occur in a language with linear types designed for implicit complexity. 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 *logarithmic space*, 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 Pierre Pradic – was published, while the semantics side is still a mere preprint (which is far from being as rigorous as I would like). Here is a talk targeted at a broad audience, that does not require prior knowledge of linear logic.

Some further material on the semantics of second-order logic in an obsolete preprint (joint work with Paolo Pistone, Thomas Seiller and Lorenzo Tortora de Falco) should be reworked in the near future with an application to automata.

## Talks (for an audience familiar with linear logic and/or denotational semantics)

- (Workshop) Linearity-TLLA 2018 short talk: abstract, slides
- Seminar in Marseille (équipe LDP), September 2018: slides
- GDRI Linear Logic plenary meeting / Chocola monthly meeting, December 2018: slides
- RIMS Logic & CS seminar, Kyoto / ERATO MMSD G0 seminar, Tokyo, March 2019: slides

## Talks (for the implicit computational complexity community)

- Final meeting of the Elica ANR project: slides
- (Workshop) DICE-FOPARA 2019: 5-page abstract, slides
- (Workshop) LCC 2019: abstract, slides

## Proof nets through the lens of graph theory

(Currently, I am not actively working on this kind of stuff, though people regularly ask me questions about it.)

By extending ideas by Christian Retoré, I provided a correspondence between graphs equipped with perfect matchings and *proof nets* for linear logic, a graphical representation of proofs. This relates the combinatorially tricky theory of proof nets with a well-studied counterpart in mainstream graph theory. The relationship is not bijective, but there are reductions in both directions preserving many structural properties (some of which were overlooked by Retoré’s pioneering work). See the paper.

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

Finally, 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*.

## Talks (for logicians)

## Talks (for graph theorists)

## Other

## Coherent interaction graphs

A rather specialized and technical paper (slides): together with Thomas Seiller, we built a variant of his interaction graphs model for multiplicative linear logic, in which the correctness criterion for proof nets admits a convincing interpretation as a non-deterministic counter-proof. That is, we revisit an idea from the early days of linear logic (cf. Girard’s*Multiplicatives*) in a more satisfactory way.

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

# Involvement in computer science teaching / outreach

## Science popularization

In 2015, Jérémy Ledent and I wrote some articles for Tangente, a French math magazine for high schoolers, on the aforementioned proofs-as-programs correspondence and on homotopy type theory.

## Prologin

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

## University teaching

In 2016, I was a teaching assistant for the Algorithms course given by Gaël Mahé at Université Paris Descartes for second-year students.

Since 2018, I have been TAing as part of my PhD at Institut Galilée, Université Paris 13.