2015/03/17 by Rick Statman
Computer Science · #cs.PL #cs.LO
paper · pdf · doi:10.4204/eptcs.177.1
published as EPTCS 177, 2015, pp. 1-9 · In Proceedings ITRS 2014, arXiv:1503.04377
arxiv created 2015/03/17 · arxiv updated 2015/03/18
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).