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

Contact / personal information:

Family name | Given name | Email address | Visual identification |
---|---|---|---|

Nguyễn | Lê Thành Dũng | `nltd at nguyentito dot eu` |
no photo available yet |

My research focuses on combinatorial and complexity-theoretic aspects of linear logic, a logical system born out of the proofs-as-programs correspondence (“Curry-Howard isomorphism”). I am particularly interested in possible connections between proof theory and other topics in computer science such as graph theory, implicit computational complexity, finite automata, descriptive complexity…

Outside of my research work, my scientific interests also span:

- Algorithms, especially combinatorial optimization (I have a master’s degree in Operations Research) and programming contest problems (both as contestant and problem-setter)
- 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, …)

This page serves as my vita (kind of). You can also download a PDF resume in French.

# Research

## Not my own work

A scan of a paper of Leivant & Marion: TODO.

A presentation on implicit complexity in the simply-typed lambda-calculus, in particular the work of Hillebrand and Kanellakis.

## Unique perfect matchings, edge-colored graphs and proof nets

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); in particular, *correctness* of a proof corresponds to *uniqueness* of a perfect matching, and *sequentializations* correspond to *bridge elimination orderings*.

I also worked on *edge-colored graphs* and *paths/trails avoiding forbidden transitions*, both as a topic of intrinsic interest and to apply them to proof nets.

- Conference paper:
*Unique perfect matchings and proof nets*, Formal Structures in Computation and Deduction 2018- Extended journal version: coming soon

- Some talks (except for the FSCD talk, all these contain information not yet published elsewhere, which will eventually appear in the aforementioned journal version):

## Around finite semantics for second-order linear logic

This joint work with Paolo Pistone, Thomas Seiller and Lorenzo Tortora de Falco is connected both to fundamental questions on second-order proof equivalence and to implicit complexity. We prove the finiteness of an observational quotient of second-order linear logic without exponentials, and deduce a characterization of regular languages in Elementary Linear Logic.

The results are currently being refined – much remains to be understood about this observational equivalence – and written up. For now, here are the slides from some early talks:

- TLLA 2018 short talk
- Seminar in Marseille
- Final meeting of the Elica ANR project (mostly about complexity; contains a conjectural characterization of logarithmic space in ELL)
- GDRI Linear Logic plenary meeting (very rough and unpolished)
- Chocola monthly meeting

## Coherent interaction graphs

This is a rather specialized and technical topic. We build a variant of Seiller’s interaction graphs 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* paper) in a more satisfactory way.

- Paper:
*Coherent interaction graphs: a nondeterministic geometry of interaction for MLL*, with Thomas Seiller (preprint) - Slides: TLLA 2018 long talk

## Other

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

## 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. See my courses webpage (French).

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

## Science popularization

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

# Resume

## Academic studies

- 2010–2012 —
*Classes préparatoires*(MPSI/MP*) in the Lycée Pierre de Fermat, Toulouse - 2012–2017 — Student in the Computer Science department at École normale supérieure
- 2018–2021 (expected) — PhD student at Université Paris 13 (see above)

## Diplomas

- 2010 —
*Baccalauréat*(high school diploma) - 2013 —
*Licence*in Computer Science — École normale supérieure de Paris / Université Paris Diderot - 2016 —
*Master*in Operations Research — Conservatoire National des Arts et Métiers - 2017 —
*Master*in Mathematics — ENS Paris-Saclay

## Programming experience

My projects: see my Github account and my Bitbucket account, or this page.

## Vanity

- 2012 — Ranked 3rd in the École Normale Supérieure entrance examination.
- 2013 — Winner of Prologin, a French national programming contest.
- 2014 — Ranked 4th in the Google Paris Hash Code contest.
- 2016 — Ranked 27th in ACM-ICPC SWERC (European programming contest).
- 2017 — Ranked 21st in the
*agrégation de mathématiques*.

## Other

I used to contribute to ENS’s student newspaper.