Welcome to my homepage! I am currently a research engineer in the SPICY team in IRISA (a public lab in Rennes, France), helping develop a proof assistant for formal verification of security protocols called Squirrel. Before that I was a graduate student in theoretical computer science at Laboratoire d’informatique de Paris Nord; you can see some of my work from this period below.
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. 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 are taking 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!
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).
Contact / personal information
|Given name:||Lê Thành Dũng|
|Visual identification:||photo (taken by Lwenn Bussière-Caraes)|
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, formal languages (finite automata / transducers / semigroups) …
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 a few programming contest problems
- 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, …)
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”. 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 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.)
The click-to-expand parts in this section use the HTML5
Expository and/or not my own work
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:
- 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
PhD thesis topic: Implicit automata in typed λ-calculi
Implicit computational complexity seeks to characterize complexity classes by using constrained programming languages. Pierre 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.
- Journées du GT Scalp (invited talk), November 2021: slides
- ICALP 2020 (pre-recorded talk): video, slides
- Inria Deducteam seminar, June 2020: slides
- Inria PARTOUT team seminar, May 2020: slides
- IRIF PhD seminar, March 2020: slides (almost no prerequisites)
- GdR IM annual ALGA meeting, October 2019: slides (for automata theorists)
- (Workshop) TLLA 2019: abstract, slides (for linear logicians)
One byproduct of the research carried out in my PhD has been to investigate automata models that compute string-to-string functions. Pradic and I have a few results about such devices (called transducers), some of which are unpublished; see the slides below.
Denotational semantics of polymorphism vs space complexity
What led me to automata (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. The semantics side is far from being as rigorous as I would like and is projected to be rewritten after I finish my PhD thesis; in the meantime, you can take a look at this old preprint. 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 can be found in in an obsolete preprint (joint work with Paolo Pistone, Thomas Seiller and Lorenzo Tortora de Falco). The Chocola talk slides below also contain some ideas that I haven’t pursued further for now.
Talks (for an audience familiar with linear logic and/or denotational semantics)
- Concurrent Games Café, January 2021: slides
- RIMS Logic & CS seminar, Kyoto / ERATO MMSD G0 seminar, Tokyo, March/April 2019: slides
- GDRI Linear Logic plenary meeting / Chocola monthly meeting, December 2018: slides
- Seminar in Marseille (équipe LDP), September 2018: slides
- (Workshop) Linearity-TLLA 2018 short talk: abstract, slides
Talks (for the implicit computational complexity community)
Combinatorics of proof nets
In a pioneering work whose significance has been underestimated in my opinion, Christian Retoré provided a translation from proof nets for linear logic, 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 (cf. list of talks).
Recently Lutz Straßburger and I have been looking at Retoré’s pomset logic (and Guglielmi’s closely related system BV, the original deep inference system) using the same tools. We just had a paper accepted at CSL 2022; see also those slides whose contents go beyond the CSL paper.
With Thomas Seiller, we also built a “geometry of interaction” model of linear logic which gives an interactive explanation of a correctness criterion by Retoré based on cographs. More recently, we realized that this could be extended to pomset logic (see the end of these slides).
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.
Talks (for logicians)
- Working group on proof nets, January 2021: slides
- “Logic beyond cographs” working group, June 2020: slides
- Seminar at Università Roma Tre, May 2019: slides
- (Conference) FSCD 2018: slides
- (Workshop) Linearity-TLLA 2018 long talk: slides
- (Workshop) DICE 2018: 5-page abstract, slides
- (Workshop) TLLA 2017: abstract, slides
Talks (for graph theorists)
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).
Involvement in computer science teaching / outreach
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.
In the 2021-2022 I am working as a teaching assistant in Université Rennes 1. I am teaching NoSQL databases this semester, and deductive program verification in the next one.
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é de Paris) for second-year students.