{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:34Z","timestamp":1750220674317,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,7,22]],"date-time":"2021-07-22T00:00:00Z","timestamp":1626912000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,7,30]]},"abstract":"<jats:p>We 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\u2013Coppo\u2013Dezani intersection type assignment system.<\/jats:p>","DOI":"10.1145\/3453481","type":"journal-article","created":{"date-parts":[[2021,7,22]],"date-time":"2021-07-22T14:10:40Z","timestamp":1626963040000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Kripke Semantics for Intersection Formulas"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1104-444X","authenticated-orcid":false,"given":"Andrej","family":"Dudenhefner","sequence":"first","affiliation":[{"name":"Saarland University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pawe\u0142","family":"Urzyczyn","sequence":"additional","affiliation":[{"name":"University of Warsaw"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,7,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2529641"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1039724889"},{"key":"e_1_2_1_4_1","unstructured":"Melvin Fitting. 1969. Intuitionistic Logic Model Theory and Forcing. North-Holland.  Melvin Fitting. 1969. Intuitionistic Logic Model Theory and Forcing. North-Holland."},{"key":"e_1_2_1_5_1","volume-title":"On 2nd order intuitionistic propositional calculus with full comprehension. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 16","author":"Gabbay Dov M.","year":"1974","unstructured":"Dov M. Gabbay . 1974. On 2nd order intuitionistic propositional calculus with full comprehension. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 16 ( 1974 ), 177\u2013186. DOI:https:\/\/doi.org\/10.1007\/bf02015377 10.1007\/bf02015377 Dov M. Gabbay. 1974. On 2nd order intuitionistic propositional calculus with full comprehension. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 16 (1974), 177\u2013186. DOI:https:\/\/doi.org\/10.1007\/bf02015377"},{"volume-title":"Semantical Investigations in Heyting\u2019s Intuitionistic Logic","author":"Gabbay Dov M.","key":"e_1_2_1_6_1","unstructured":"Dov M. Gabbay . 1981. Semantical Investigations in Heyting\u2019s Intuitionistic Logic . Synthese Library , Vol . 148. D. Reidel. DOI:https:\/\/doi.org\/10.1007\/978-94-017-2977-2 10.1007\/978-94-017-2977-2 Dov M. Gabbay. 1981. Semantical Investigations in Heyting\u2019s Intuitionistic Logic. Synthese Library, Vol. 148. D. Reidel. DOI:https:\/\/doi.org\/10.1007\/978-94-017-2977-2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exaa055"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/187812.187947"},{"key":"e_1_2_1_9_1","volume-title":"4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), Herman Geuvers (Ed.)","volume":"131","author":"Liquori Luigi","year":"2019","unstructured":"Luigi Liquori and Claude Stolze . 2019 . The Delta-calculus: Syntax and types . In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), Herman Geuvers (Ed.) , Vol. 131 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Article 28, 20 pages. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2019.28 10.4230\/LIPIcs.FSCD.2019.28 Luigi Liquori and Claude Stolze. 2019. The Delta-calculus: Syntax and types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), Herman Geuvers (Ed.), Vol. 131. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, Article 28, 20 pages. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.28"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2594832.2594842"},{"volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Pottinger Garrel","key":"e_1_2_1_12_1","unstructured":"Garrel Pottinger . 1980. A type assignment for the strongly normalizable -terms . In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , J. P. Seldin and J. R. Hindley (Eds.). Academic Press , 561\u2013577. Garrel Pottinger. 1980. A type assignment for the strongly normalizable -terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, 561\u2013577."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737252"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 5th Workshop on Intersection Types and Related Systems (ITRS\u201910)","volume":"45","author":"Della Rocca Simona Ronchi","year":"2010","unstructured":"Simona Ronchi Della Rocca , Alexis Saurin , Yiorgos Stavrinos , and Anastasia Veneti . 2010 . Intersection logic in sequent calculus style . In Proceedings of the 5th Workshop on Intersection Types and Related Systems (ITRS\u201910) , Vol. 45 . 16\u201330. I DOI:https:\/\/doi.org\/10.4204\/EPTCS.45.2 10.4204\/EPTCS.45.2 Simona Ronchi Della Rocca, Alexis Saurin, Yiorgos Stavrinos, and Anastasia Veneti. 2010. Intersection logic in sequent calculus style. In Proceedings of the 5th Workshop on Intersection Types and Related Systems (ITRS\u201910), Vol. 45. 16\u201330. I DOI:https:\/\/doi.org\/10.4204\/EPTCS.45.2"},{"key":"e_1_2_1_15_1","first-page":"69","article-title":"The intuitionistic propositional calculus with quantifiers","volume":"22","author":"Sobolev S. K.","year":"1977","unstructured":"S. K. Sobolev . 1977 . The intuitionistic propositional calculus with quantifiers . Mathematical Notes of the Academy of Sciences of the USSR 22 , 1 (1977), 69 \u2013 76 . DOI:https:\/\/doi.org\/10.1007\/bf01147694 10.1007\/bf01147694 S. K. Sobolev. 1977. The intuitionistic propositional calculus with quantifiers. Mathematical Notes of the Academy of Sciences of the USSR 22, 1 (1977), 69\u201376. DOI:https:\/\/doi.org\/10.1007\/bf01147694","journal-title":"Mathematical Notes of the Academy of Sciences of the USSR"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586625"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1922521.1922537"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-016-9661-4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00089-0"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.2.109"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00356-X"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453481","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:07Z","timestamp":1750197787000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453481"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,22]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,30]]}},"alternative-id":["10.1145\/3453481"],"URL":"https:\/\/doi.org\/10.1145\/3453481","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,7,22]]},"assertion":[{"value":"2020-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}