Search

• < Previous
• 1
• Next >

---

Intersection Types for the lambda-mu Calculus

Steffen van Bakel ; Franco Barbanera ; Ugo de'Liguoro.

We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach.&nbsp;[&hellip;]

---

Adding Negation to Lambda Mu

Steffen van Bakel.

We present $\cal L$, an extension of Parigot's $\lambda\mu$-calculus by adding negation as a type constructor, together with syntactic constructs that represent negation introduction and elimination. We will define a notion of reduction that extends $\lambda\mu$'s reduction system with two new&nbsp;[&hellip;]

---