5 citations · 19 across the 10 of their papers we have counts for
13 papers
The structure of polynomial growth for tree automata/transducers and MSO set queries
Paul Gallot, Nathan Lhote, Lê Thành Dũng Nguyên
Given an -weighted tree automaton, we give a decision procedure for exponential vs polynomial growth (with respect to the input size) in quadratic time, and an algorith…
On the complexity of normalization for the planar -calculus
Anupam Das, Damiano Mazza, Lê Thành Dũng Nguyên +1
We sketch a tentative proof of P-completeness for the -convertibility problem on untyped planar (a.k.a. ordered or non-commutative) -terms.
Function spaces for orbit-finite sets
Mikołaj Bojańczyk, Lê Thành Dũng Nguyên, Rafał Stefański
Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they d…
Slightly Non-Linear Higher-Order Tree Transducers
Lê Thành Dũng Nguyên, Gabriele Vanoni
We investigate the tree-to-tree functions computed by "affine -transducers": tree automata whose memory consists of an affine -term instead of a finite state. They can be see…
Syntactically and semantically regular languages of lambda-terms coincide through logical relations
Vincent Moreau, Lê Thành Dũng Nguyên
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of…
Two-way automata and transducers with planar behaviours are aperiodic
Lê Thành Dũng Nguyên, Camille Noûs, Cécilia Pradic
We consider a notion of planarity for two-way finite automata and transducers, inspired by Temperley-Lieb monoids of planar diagrams. We show that this restriction captures star-fr…
Simply typed convertibility is TOWER-complete even for safe lambda-terms
Lê Thành Dũng Nguyên
We consider the following decision problem: given two simply typed -terms, are they -convertible? Equivalently, do they have the same normal form? It is famously non-elementa…
A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
Lê Thành Dũng Nguyên, Lutz Straßburger
Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originate…
Complexity of correctness for pomset logic proof nets
Lê Thành Dũng Nguyên
We show that it is coNP-complete to decide whether a given proof structure of pomset logic is a correct proof net, using the graph-theoretic used in a previous paper of ours (arXiv…
Coherent Interaction Graphs
Lê Thành Dũng Nguyen, Thomas Seiller
We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic (MLL) extended with non-determinism. Thanks t…
Around finite second-order coherence spaces
Lê Thành Dũng Nguyên
Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhib…
Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix
Lê Thành Dũng Nguyên
This 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 pr…
Constrained path-finding and structure from acyclicity
Lê Thành Dũng Nguyên
This note presents several results in graph theory inspired by the author's work in the proof theory of linear logic; these results are purely combinatorial and do not involve logi…