7 citations · 16 across the 7 of their papers we have counts for
7 papers
On Statman's Finite Completeness Theorem
Richard Statman, Gilles Dowek
We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the -definability conjecture implies the higher-…
Uniqueness typing for intersection types
Richard Statman, Andrew Polonsky
Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Veneri [1981], we prove several facts about sets of terms having a given intersecti…
Products in a Category with Only One Object
Richard Statman
We consider certain decision problems for the free model of the theory of Cartesian monoids. We introduce a model of computation based on the notion of a single stack one-way PDA d…
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 intersect…
A Finite Model Property for Intersection Types
Rick Statman
We show that the relational theory of intersection types known as BCD has the finite model property; that is, BCD is complete for its finite models. Our proof uses rewriting techni…
The Omega Rule is -Complete in the -Calculus
Benedetto Intrigila, Richard Statman
In a functional calculus, the so called Ω-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.…