Search

• < Previous
• 1
• Next >

---

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus

Beniamino Accattoli ; Delia Kesner.

Inspired by a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda j, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and&nbsp;[&hellip;]

---

(Leftmost-Outermost) Beta Reduction is Invariant, Indeed

Beniamino Accattoli ; Ugo Dal Lago.

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete&nbsp;[&hellip;]

---

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic

Beniamino Accattoli.

This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by&nbsp;[&hellip;]

---