{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,2]],"date-time":"2026-03-02T11:19:20Z","timestamp":1772450360702,"version":"3.50.1"},"reference-count":108,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,29]]},"DOI":"10.1109\/lics52264.2021.9470508","type":"proceedings-article","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T20:14:07Z","timestamp":1625688847000},"page":"1-15","source":"Crossref","is-referenced-by-count":4,"title":["G\u00f6del-McKinsey-Tarski and Blok-Esakia for Heyting-Lewis Implication"],"prefix":"10.1109","author":[{"given":"Jim","family":"de Groot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tadeusz","family":"Litak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"ref32","first-page":"383","article-title":"On an intuitionistic modal logic","volume":"65","author":"bierman","year":"2000","journal-title":"Studia Logica An International Journal for Symbolic Logic"},{"key":"ref31","first-page":"292","article-title":"Categorical and kripke semantics for constructive S4 modal logic","volume":"2142","author":"alechina","year":"2001","journal-title":"Proc CSL 2001 ser Lecture Notes in Computer Science"},{"key":"ref30","first-page":"113","article-title":"Intuitionistic modal logic with quantifiers","volume":"7","author":"fitch","year":"1948","journal-title":"Portugaliae Mathematica"},{"key":"ref37","first-page":"exaa082","article-title":"Categorical and algebraic aspects of the intuitionistic modal logic IEL? and its predicate extensions","volume":"12","author":"rogozin","year":"2020","journal-title":"Journal of Logic and Computation"},{"key":"ref36","first-page":"27:1","article-title":"Negative Translations and Normal Modality","volume":"84","author":"litak","year":"0"},{"key":"ref35","first-page":"411","article-title":"Basic constructive modality","author":"de paiva","year":"2011","journal-title":"Logic Without Frontiers- Festschrift for Walter Alexandre Carnielli on the occasion of his 60th birthday"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680500568X"},{"key":"ref28","article-title":"Dual-Context Calculi for Modal Logic","volume":"16","author":"kavvos","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-8860-1_8"},{"key":"ref29","first-page":"139","article-title":"Modal theories with intuitionistic logic","author":"sotirov","year":"1980","journal-title":"Mathematical Logic Proc Conf Math Logic Dedicated to the Memory of A A Markov (1903 - 1979)"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzi047"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.2977\/prims\/1195189604"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.2307\/2266613"},{"key":"ref24","article-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","author":"simpson","year":"1994","journal-title":"Ph D Dissertation"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF02429840","article-title":"Models for normal intuitionistic modal logics","volume":"43","author":"bo\u017ei?","year":"1984","journal-title":"Studia Logica"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-018-9471-4"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.439"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2014.07.005"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2109-7_17"},{"key":"ref50","first-page":"3","article-title":"Compiling functional types to relational specifications for low level imperative code","author":"benton","year":"2009","journal-title":"Types in Language Design and Implementation (TLDI'07)"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"ref59","first-page":"73","article-title":"Programming with arrows","volume":"3622","author":"hughes","year":"2004","journal-title":"Revised Lectures AFP 2004 ser Lecture Notes in Computer Science"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_9"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_8"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034782"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.38"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.49"},{"key":"ref40","first-page":"1035","article-title":"Cover semantics for quantified lax logic","author":"goldblatt","year":"2010","journal-title":"J Log Comput"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.indag.2017.10.003"},{"key":"ref3","author":"lewis","year":"1932","journal-title":"Symbolic Logic"},{"key":"ref6","article-title":"Logic and pragmatism","volume":"2","author":"lewis","year":"1930","journal-title":"Contemporary American Philosophy Personal Statements ser Library of philosophy"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2940598"},{"key":"ref8","author":"becker","year":"1930","journal-title":"Zur Logik der Modalitäten ser Jahrbuch für Philosophie und phänomenologische Forschung"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45500-0_8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093893933"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"481","DOI":"10.5840\/monist19324241","article-title":"Alternative systems of logic","volume":"42","author":"lewis","year":"1932","journal-title":"The Monist"},{"key":"ref46","author":"boolos","year":"1993","journal-title":"Provability in Logic"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1475"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"ref47","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0003-4843(82)90024-9","article-title":"On the completeness principle: A study of provability in Heyting Arithmetic and extensions","volume":"22","author":"visser","year":"1982","journal-title":"Ann Math Logic"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00169-7"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.18"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002998"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/BF02123402"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1007\/BF02125226"},{"key":"ref71","doi-asserted-by":"crossref","first-page":"997","DOI":"10.1016\/j.apal.2018.05.001","article-title":"The ?1 provability logic of HA","volume":"169","author":"ardeshir","year":"2018","journal-title":"Ann of Pure Appl Logic"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1230396766"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-8301-9"},{"key":"ref77","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1093\/oso\/9780198538622.003.0008","article-title":"Embeddings of Heyting algebras","author":"de jongh","year":"1996","journal-title":"Logic From Foundations to Applications"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370383"},{"key":"ref75","first-page":"14","article-title":"Löb’s logic meets the µ-calculus","volume":"3838","author":"visser","year":"2005","journal-title":"Processes Terms and Cycles Steps on the Road to Infinity Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday ser LNCS"},{"key":"ref78","doi-asserted-by":"crossref","first-page":"1118","DOI":"10.1017\/jsl.2019.44","article-title":"The ?1-provability logic of HA?","volume":"84","author":"ardeshir","year":"2019","journal-title":"J Symb Log"},{"key":"ref79","volume":"77","author":"blok","year":"1989","journal-title":"Algebraizable logics ser Memoirs AMS"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.02.014"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680999027X"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007308"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.02.018"},{"key":"ref64","article-title":"Lewisian fixed points I: two incomparable constructions","author":"litak","year":"2019","journal-title":"CoRR"},{"key":"ref65","author":"visser","year":"1994","journal-title":"Propositional combinations of ?-sentences in Heyting’s Arithmetic ser Logic Group Preprint Series 117"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00081-1"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757006"},{"key":"ref68","article-title":"A modal analysis of some principles of the provability logic of Heyting Arithmetic","volume":"2","author":"iemhoff","year":"2001","journal-title":"Proceedings of AiML’98"},{"key":"ref2","doi-asserted-by":"crossref","DOI":"10.1525\/9780520398252","author":"lewis","year":"1918","journal-title":"A Survey of Symbolic Logic"},{"key":"ref69","article-title":"Provability logic and admissible rules","author":"iemhoff","year":"2001","journal-title":"Ph D Dissertation"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.2307\/2012652"},{"key":"ref95","first-page":"63","article-title":"On intuitionistic modal epistemic logic","volume":"21","author":"williamson","year":"1992","journal-title":"Journal of Philosophical Logic"},{"key":"ref108","doi-asserted-by":"publisher","DOI":"10.1002\/malq.201500030"},{"key":"ref94","article-title":"Algorithmic methods for non-classical logics","author":"georgiev","year":"2017","journal-title":"Ph D Dissertation"},{"key":"ref107","first-page":"1","article-title":"Complexity of the interpretability logic IL","volume":"27","author":"mikec","year":"2019","journal-title":"Log J IGPL"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(1:5)2006"},{"key":"ref106","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1093\/jigpal\/jzx027","article-title":"Decidability of interpretability logics ILM0 and ILW?","volume":"25","author":"mikec","year":"2017","journal-title":"Logic Journal of the IGPL"},{"key":"ref92","author":"blackburn","year":"2001","journal-title":"Modal Logic Cambridge Tracts in Theoretical Computer Science"},{"key":"ref105","first-page":"31","author":"de jongh","year":"1990","journal-title":"Provability Logics for Relative Interpretability"},{"key":"ref91","first-page":"108","article-title":"Kripke type semantics for propositional modal logics with intuitionistic base","volume":"199","author":"shehtman","year":"0","journal-title":"Modal and Tense Logics"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1007\/BF02121259"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-019-09538-4"},{"key":"ref102","article-title":"Frontiers of conditional logic","author":"weiss","year":"2019","journal-title":"Ph D Dissertation"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394807"},{"key":"ref99","article-title":"Goldblatt-thomason theorems for modal intuitionistic logics","author":"de groot","year":"2020"},{"key":"ref96","doi-asserted-by":"crossref","first-page":"877","DOI":"10.1007\/s10992-011-9207-1","article-title":"Intuitionistic epistemic logic, kripke models and fitch’s paradox","volume":"41","author":"proietti","year":"2012","journal-title":"Journal of Philosophical Logic"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:17)2013"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511520006"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020315000374"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200410022"},{"key":"ref14","article-title":"Varieties of interior algebras","author":"blok","year":"1976","journal-title":"Ph D Dissertation"},{"key":"ref15","first-page":"257","article-title":"On varieties of Grzegorczyk algebras","author":"esakia","year":"1979","journal-title":"Studies in non-classical logics and set theory"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-12096-2"},{"key":"ref82","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s11225-006-7196-9","article-title":"Beyond Rasiowa’s algebraic approach to non-classical logics","volume":"82","author":"font","year":"2006","journal-title":"Studies in Logic"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BF02672476"},{"key":"ref81","author":"rasiowa","year":"1974","journal-title":"An Algebraic Approach to Non-Classical Logics"},{"key":"ref18","first-page":"168","article-title":"Intuitionistic modal logics as fragments of classical bimodal logics","author":"wolter","year":"1998","journal-title":"Logic at Work Essays in honour of Helena Rasiowa"},{"key":"ref84","first-page":"147","article-title":"Topological Kripke models","volume":"15","author":"esakia","year":"1974","journal-title":"Soviet Mathematics Doklady"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200310023"},{"key":"ref83","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","author":"chagrov","year":"1997","journal-title":"Modal Logic"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024621922509"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1007\/BF01463150"},{"key":"ref85","article-title":"Lattices of intermediate and cylindric modal logics","author":"bezhanishvili","year":"2006","journal-title":"Ph D Dissertation"},{"key":"ref86","first-page":"39","article-title":"Einde Interpretation des intuitionistischen Aussagenkalkuls","volume":"6","author":"g\u00f6del","year":"1933","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.2307\/2268135"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19590051405"}],"event":{"name":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","location":"Rome, Italy","start":{"date-parts":[[2021,6,29]]},"end":{"date-parts":[[2021,7,2]]}},"container-title":["2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9470497\/9470501\/09470508.pdf?arnumber=9470508","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T16:45:46Z","timestamp":1725381946000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9470508\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":108,"URL":"https:\/\/doi.org\/10.1109\/lics52264.2021.9470508","relation":{},"subject":[],"published":{"date-parts":[[2021,6,29]]}}}