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;]

---

A Theory of Explicit Substitutions with Safe and Full Composition

Delia Kesner.

Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in&nbsp;[&hellip;]

---

Non-idempotent types for classical calculi in natural deduction style

Delia Kesner ; Pierre Vial.

In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize&nbsp;[&hellip;]

---

Solvability = Typability + Inhabitation

Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca.

We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabitation in an intersection type system P based on non-idempotent types. We show first that the system P characterizes the&nbsp;[&hellip;]

---

Inhabitation for Non-idempotent Intersection Types

Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca.

The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the&nbsp;[&hellip;]

---

Node Replication: Theory And Practice

Delia Kesner ; Loïc Peyrot ; Daniel Ventura.

We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

---

A Strong Bisimulation for a Classical Term Calculus

Eduardo Bonelli ; Delia Kesner ; Andrés Viso.

When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $\lambda$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on $\lambda$-terms known as $\simeq_\sigma$-equivalence, in both the&nbsp;[&hellip;]

---

A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications

José Espírito Santo ; Delia Kesner ; Loïc Peyrot.

We introduce a call-by-name lambda-calculus $\lambda Jn$ with generalized applications which is equipped with distant reduction. This allows to unblock $\beta$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $\Lambda J$-calculus with&nbsp;[&hellip;]

---