Search

• < Previous
• 1
• Next >

---

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 originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs,&nbsp;[&hellip;]

---

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 $\lambda$-terms, are they $\beta$-convertible? Equivalently, do they have the same normal form? It is famously non-elementary, but the precise complexity - namely TOWER-complete - is lesser known. One goal of this short paper is to&nbsp;[&hellip;]

---

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\'e (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&nbsp;[&hellip;]

---