Artykuł w czasopiśmie
Brak miniatury
Licencja
CC-BYCC-BY - Uznanie autorstwa
 

Kripke Semantics for Intersection Formulas

Uproszczony widok
dc.abstract.enWe propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, 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.
dc.affiliationUniwersytet Warszawski
dc.contributor.authorDudenhefner, Andrej
dc.contributor.authorUrzyczyn, Paweł
dc.date.accessioned2024-01-25T04:57:30Z
dc.date.available2024-01-25T04:57:30Z
dc.date.copyright2021-06-28
dc.date.issued2021
dc.description.accesstimeAT_PUBLICATION
dc.description.financeŚrodki finansowe przyznane na realizację projektu w zakresie badań naukowych lub prac rozwojowych
dc.description.number3
dc.description.versionFINAL_PUBLISHED
dc.description.volume22
dc.identifier.doi10.1145/3453481
dc.identifier.issn1529-3785
dc.identifier.urihttps://repozytorium.uw.edu.pl//handle/item/110659
dc.identifier.weblinkhttps://dl.acm.org/doi/pdf/10.1145/3453481
dc.languageeng
dc.pbn.affiliationcomputer and information sciences
dc.relation.ispartofACM Transactions on Computational Logic
dc.relation.pages1-16
dc.rightsCC-BY
dc.sciencecloudnosend
dc.titleKripke Semantics for Intersection Formulas
dc.typeJournalArticle
dspace.entity.typePublication