A Finite Model Property for Intersection Types
Programming Languages
2015-03-18 v1 Logic in Computer Science
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).
Keywords
Cite
@article{arxiv.1503.04906,
title = {A Finite Model Property for Intersection Types},
author = {Rick Statman},
journal= {arXiv preprint arXiv:1503.04906},
year = {2015}
}
Comments
In Proceedings ITRS 2014, arXiv:1503.04377