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…