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||Visual identification|
|Nguyễn||Lê Thành Dũng||
||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 and transducers, descriptive complexity…
Outside of my research work, my scientific interests also span:
- Algorithms, especially complexity theory and combinatorial optimization (I have a master’s degree in Operations Research)
- 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 (last updated May 2019) in French.
Full list of publications: see my dblp page.
The click-to-expand parts in this section use the HTML5
Not my own work
A scan of a paper of Leivant & Marion: TODO.
Some slides on the expressivity of the simply-typed λ-calculus:
- on Hillebrand and Kanellakis’s work in implicit complexity, at a GdR IM working group meeting
- on the definable functions on Church encodings, very short talk (10 minutes) at the TACL 2019 summer school
Unique perfect matchings, edge-colored graphs and proof nets
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.
Description 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.
- (Journal submission) Unique perfect matchings, edge-colored graphs and proof nets for linear logic with Mix, invited to LMCS, 2019 (currently being revised)
Long version of conference paper Unique perfect matchings and proof nets, FSCD 2018
AbstractThis paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms.
Alternating cycles in perfect matchings serve as witnesses of non-uniqueness, and in this significantly expanded journal version, we discuss connections with other kinds of constrained cycles known to be equivalent: semicycles in directed graphs, trails avoiding forbidden transitions, and properly colored cycles in edge-colored graphs. While the second one provides an explanation and generalization of Retoré’s “R&B-graphs”, the latter leads us to prove the coNP-hardness of Pagani’s visible acyclicity criterion for MELL proof nets. We also connect Lamarche’s essential nets to R&B-graphs.
- (arXiv note) Constrained path-finding and structure from acyclicity, 2019
Talks (for logicians)
Talks (for graph theorists)
Revisiting implicit complexity in linear logic with finite semantics of polymorphism and automata theory
Description It is hard to summarize this research project, and the order of publication is all messed up relatively to both the order of discovery and the logical dependencies.
Basically, we are working at the confluence of:
- the semantic evaluation techniques used to analyze the computational complexity properties of the simply typed λ-calculus, which we adapt to other settings
- the connection between Church encodings and automata, mediated by semantics, whose fruitfulness has been previously demonstrated in higher-order model checking
- the treatment of polymorphism by means of normal functors in stable domain theory, which entail finiteness and effectivity properties that had not been exploited before
- the combinatorial study of (second-order) proof nets and the geometry of interaction
This leads, for instance, to characterizations in (variants of) linear logic of
- logarithmic space queries over finite relational structures (with linear orders)
- regular string functions, a.k.a. MSO-definable transductions
- (Conference paper) From normal functors to logarithmic space queries, with Pierre Pradic, ICALP 2019
AbstractWe introduce a new approach to implicit complexity in linear logic, inspired by functional database query languages and using recent developments in effective denotational semantics of polymorphism. We give the first sub-polynomial upper bound in a type system with impredicative polymorphism; adding restrictions on quantifiers yields a characterization of logarithmic space, for which extensional completeness is established via descriptive complexity.
- (Submitted to worskhop post-proceedings) On the elementary affine λ-calculus with and without type fixpoints
AbstractThe elementary affine λ-calculus was introduced as a polyvalent setting for implicit computational complexity, allowing for characterizations of polynomial time and hyperexponential time predicates. But these results rely on type fixpoints (a.k.a. recursive types), and it was unknown whether this feature of the type system was really necessary. We give a positive answer by showing that without type fixpoints, we get a characterization of regular languages instead of polynomial time. The proof uses the semantic evaluation method. We also propose an aesthetic improvement on the characterization of the function classes FP and k-FEXPTIME in the presence of recursive types.
- (arXiv preprint) Around finite second-order coherence spaces
AbstractMany applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhibit such a finite semantics for a polymorphic purely linear language: more precisely, we show that in Girard’s semantics of second-order linear logic using coherence spaces and normal functors, the denotations of multiplicative-additive formulas are finite.
This model is also effective, in the sense that the denotations of formulas and proofs are computable, as we show. We also establish analogous results for a second-order extension of Ehrhard’s hypercoherences; while finiteness holds for the same reason as in coherence spaces, effectivity presents additional difficulties.
Finally, we discuss the applications our our work to implicit computational complexity in linear (or affine) logic. In view of these applications, we study cardinality and complexity bounds in our finite semantics.
- (arXiv preprint) Typed λ-calculi and superclasses of regular transductions
I convinced myself that this was not the right way to introduce things. But for now, it is the only reference for some of my ideas on transducers.
- Some material on proof nets 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 transductions.
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 2019: slides
- RIMS Logic & CS seminar, Kyoto / ERATO MMSD G0 seminar, Tokyo, March 2019: slides
- (Workshop) TLLA 2019: abstract, slides
Talks (for the implicit computational complexity community)
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.
The work was presented at the Linearity-TLLA 2018 joint workshop, and published in its post-proceedings.
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
In 2016, I was a teaching assistant for the Algorithms course given by Gaël Mahé at Université Paris Descartes for second-year students.
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.
- 2010–2012 — Classes préparatoires (MPSI/MP* : maths/physics/compsci) in the Lycée Pierre de Fermat, Toulouse
- 2012–2017 — Student at École normale supérieure (major in Computer Science, minor in Mathematics)
- 2018–2021 (expected) — PhD student at Université Paris 13 (see above)
- 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
- 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.
I used to contribute to ENS’s student newspaper.