We propose a notion of Kripke-style model for intersection logic. Using a game interpretation we prove soundness and completeness of the proposed semantics. That is, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.
Download PDF Show BibTeX
Login to edit