Publication details

Saarland University Computer Science

Kripke Semantics for Intersection Formulas

Andrej Dudenhefner, Paweł Urzyczyn

Transactions on Computational Logic 22(3):15:1-15:16, 2021

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

Legal notice, Privacy policy