paper

A Finite Model Property for Intersection Types

arXiv:1503.04906 · doi:10.4204/EPTCS.177.1

Abstract

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 techniques which have as an immediate by-product the polynomial time decidability of the preorder <= (although this also follows from the so called beta soundness of BCD).

In Proceedings ITRS 2014, arXiv:1503.04377

A Finite Model Property for Intersection Types · wovepaper