5 citations · 19 across the 10 of their papers we have counts for
9 papers · 1 filter
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…
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…
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…