Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@ARTICLE{DudenhefnerUrzyczyn:2021:Kripke,
  title = {Kripke Semantics for Intersection Formulas},
  author = {Andrej Dudenhefner and Paweł Urzyczyn},
  year = {2021},
  publisher = {ACM},
  journal = {Transactions on Computational Logic},
  volume = {22},
  pages = {15:1-15:16},
  number = {3},
}

Login to edit