A Finite Model Property for Intersection Types
Author: Richard Statman
Paper Information
| Title: | A Finite Model Property for Intersection Types |
| Authors: | Richard Statman |
| Proceedings: | ITRS 2014 Proceedings |
| Editors: | Jakob Rehof and Moritz Martens |
| Keywords: | intersection types, rewriting techniques, finite model property |
| Abstract: | 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 soundeness of BCD). |
| Pages: | 0 |
| Talk: | Jul 18 10:45 |
| Paper: |  |