Search

• < Previous
• 1
• Next >

---

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

Jose Espirito Santo ; Ralph Matthes ; Luis Pinto.

The intuitionistic fragment of the call-by-name version of Curien and Herbelin's \lambda\_mu\_{\~mu}-calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed lambda-calculus. Our embedding is a continuation-and-garbage-passing style translation, 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;]

---