Search

• < Previous
• 1
• Next >

---

On sets of terms having a given intersection type

Andrew Polonsky ; Richard Statman.

Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair&nbsp;[&hellip;]

---

The Omega Rule is $\mathbf{\Pi_{1}^{1}}$-Complete in the $\lambda\beta$-Calculus

Benedetto Intrigila ; Richard Statman.

In a functional calculus, the so called \Omega-rule states that if two terms P and Q applied to any closed term <i>N</i> return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the \lambda\beta-calculus the \Omega-rule does not hold, even when the&nbsp;[&hellip;]

---

Solution of a Problem of Barendregt on Sensible lambda-Theories

Benedetto Intrigila ; Richard Statman.

<i>H</i> is the theory extending &#946;-conversion by identifying all closed unsolvables. <i>H</i>&#969; is the closure of this theory under the &#969;-rule (and &#946;-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of <i>H</i>&#969; form&nbsp;[&hellip;]

---