{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T20:28:21Z","timestamp":1770236901724,"version":"3.49.0"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003407","name":"Ministero dell\u2019Istruzione, dell\u2019Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["201784YSZ5"],"award-info":[{"award-number":["201784YSZ5"]}],"id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["818616"],"award-info":[{"award-number":["818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent, usage-sensitive computations, especially when combined with computational effects. From a semantic perspective, effectful and coeffectful languages have been studied mostly by means of denotational semantics and almost nothing has been done from the point of view of relational reasoning. This gap in the literature is quite surprising, since many cornerstone results \u2014 such as<jats:italic>non-interference<\/jats:italic>,<jats:italic>metric preservation<\/jats:italic>, and<jats:italic>proof irrelevance<\/jats:italic>\u2014 on concrete coeffects are inherently relational. In this paper, we fill this gap by developing a general theory and calculus of program relations for higher-order languages with combined effects and coeffects. The relational calculus builds upon the novel notion of a<jats:italic>corelator<\/jats:italic>(or<jats:italic>comonadic lax extension<\/jats:italic>) to handle coeffects relationally. Inside such a calculus, we define three notions of effectful and coeffectful program refinements:<jats:italic>contextual approximation<\/jats:italic>,<jats:italic>logical preorder<\/jats:italic>, and<jats:italic>applicative similarity<\/jats:italic>. These are the first operationally-based notions of program refinement (and, consequently, equivalence) for languages with combined effects and coeffects appearing in the literature. We show that the axiomatics of a corelator (together with the one of a relator) is precisely what is needed to prove all the aforementioned program refinements to be precongruences, this way obtaining compositional relational techniques for reasoning about combined effects and coeffects.<\/jats:p>","DOI":"10.1145\/3498692","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["A relational theory of effects and coeffects"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Gavazzo","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_2_2_3_1","volume-title":"Research Topics in Functional Programming","author":"Abramsky S.","unstructured":"S. Abramsky . 1990. The Lazy Lambda Calculus . In Research Topics in Functional Programming , D. Turner (Ed.). Addison Wesley , 65\u2013117. S. Abramsky. 1990. The Lazy Lambda Calculus. In Research Topics in Functional Programming, D. Turner (Ed.). Addison Wesley, 65\u2013117."},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science. Clarendon Press 1\u2013168. S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science. Clarendon Press 1\u2013168.","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_2_8_1","volume-title":"Voermans, and Jaap van der Woude","author":"Backhouse Roland Carl","year":"1991","unstructured":"Roland Carl Backhouse , Peter J. de Bruin , Paul F. Hoogendijk , Grant Malcolm , Ed Voermans, and Jaap van der Woude . 1991 . Polynomial Relators (Extended Abstract). In Proc. of (AMAST \u201991 (Workshops in Computing). Springer , 303\u2013326. Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. 1991. Polynomial Relators (Extended Abstract). In Proc. of (AMAST \u201991 (Workshops in Computing). Springer, 303\u2013326."},{"key":"e_1_2_2_9_1","unstructured":"H.P. Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland. H.P. Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060439"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561458"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2015.567"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:APCS.0000018144.87456.10"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_10"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.007"},{"key":"e_1_2_2_23_1","volume-title":"Proc. of ICTCS","author":"Lago Ugo Dal","year":"2020","unstructured":"Ugo Dal Lago and Francesco Gavazzo . 2020 . Differential Logical Relations Part II: Increments and Derivatives . In Proc. of ICTCS 2020. 101\u2013114. Ugo Dal Lago and Francesco Gavazzo. 2020. Differential Logical Relations Part II: Increments and Derivatives. In Proc. of ICTCS 2020. 101\u2013114."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.09.027"},{"key":"e_1_2_2_25_1","volume-title":"via Lawvere. CoRR, abs\/2103.03871","author":"Lago Ugo Dal","year":"2021","unstructured":"Ugo Dal Lago and Francesco Gavazzo . 2021. Modal Reasoning = Metric Reasoning , via Lawvere. CoRR, abs\/2103.03871 ( 2021 ), arxiv:2103.03871 Ugo Dal Lago and Francesco Gavazzo. 2021. Modal Reasoning = Metric Reasoning, via Lawvere. CoRR, abs\/2103.03871 (2021), arxiv:2103.03871"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.23"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498680"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_2_29_1","volume-title":"Proc. of ICTCS","author":"Lago Ugo Dal","year":"2017","unstructured":"Ugo Dal Lago , Francesco Gavazzo , and Ryo Tanaka . 2017 . Effectful Applicative Similarity for Call-by-Name Lambda Calculi . In Proc. of ICTCS 2017. 87\u201398. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2017. Effectful Applicative Similarity for Call-by-Name Lambda Calculi. In Proc. of ICTCS 2017. 87\u201398."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.025"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.111"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785715"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209149"},{"key":"e_1_2_2_38_1","volume-title":"Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation","author":"Gavazzo Francesco","unstructured":"Francesco Gavazzo . 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation . University of Bologna , Italy. http:\/\/amsdottorato.unibo.it\/9075\/ Francesco Gavazzo. 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation. University of Bologna, Italy. http:\/\/amsdottorato.unibo.it\/9075\/"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3573-9_6"},{"key":"e_1_2_2_44_1","volume-title":"Functional programming and input\/output. Ph. D. Dissertation","author":"Gordon Andrew Donald","unstructured":"Andrew Donald Gordon . 1992. Functional programming and input\/output. Ph. D. Dissertation . University of Cambridge , UK. Andrew Donald Gordon. 1992. Functional programming and input\/output. Ph. D. Dissertation. University of Cambridge, UK."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007172"},{"key":"e_1_2_2_46_1","volume-title":"Practical Foundations for Programming Languages (2nd. Ed.)","author":"Harper Robert","unstructured":"Robert Harper . 2016. Practical Foundations for Programming Languages (2nd. Ed.) . Cambridge University Press . Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press."},{"key":"e_1_2_2_47_1","first-page":"113","article-title":"A cottage industry of lax extensions","volume":"3","author":"Hoffman D.","year":"2015","unstructured":"D. Hoffman . 2015 . A cottage industry of lax extensions . Categories and General Algebraic Structures with Applications , 3 , 1 (2015), 113 \u2013 151 . D. Hoffman. 2015. A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications, 3, 1 (2015), 113\u2013151.","journal-title":"Categories and General Algebraic Structures with Applications"},{"key":"e_1_2_2_48_1","volume-title":"A Categorical Approach to Order, Metric, and Topology","author":"Topology Monoidal","unstructured":"2014. Monoidal Topology . A Categorical Approach to Order, Metric, and Topology , D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press . 2014. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_6"},{"key":"e_1_2_2_53_1","first-page":"275","article-title":"Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A","volume":"27","author":"Kawahara Yasuo","year":"1973","unstructured":"Yasuo Kawahara . 1973 . Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A , Mathematics , 27 , 2 (1973), 275 \u2013 289 . Yasuo Kawahara. 1973. Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A, Mathematics, 27, 2 (1973), 275\u2013289.","journal-title":"Mathematics"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01703261"},{"key":"e_1_2_2_55_1","unstructured":"S.B. Lassen. 1998. Relational Reasoning About Contexts. In Higher Order Operational Techniques in Semantics Andrew D. Gordon and Andrew M. Pitts (Eds.). 91\u2013136. S.B. Lassen. 1998. Relational Reasoning About Contexts. In Higher Order Operational Techniques in Semantics Andrew D. Gordon and Andrew M. Pitts (Eds.). 91\u2013136."},{"key":"e_1_2_2_56_1","volume-title":"Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Dept. of Computer Science","author":"Lassen S.B.","unstructured":"S.B. Lassen . 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Dept. of Computer Science , University of Aarhus. S.B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Dept. of Computer Science, University of Aarhus."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80083-5"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.15"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02924844"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_2_61_1","volume-title":"Categories for the Working Mathematician","author":"MacLane S.","unstructured":"S. MacLane . 1971. Categories for the Working Mathematician . Springer-Verlag . S. MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1460690.1460715"},{"key":"e_1_2_2_65_1","volume-title":"Proc. of IFIP","author":"McCarthy John","year":"1962","unstructured":"John McCarthy . 1962 . Towards a Mathematical Science of Computation . In Proc. of IFIP 1962. 21\u201328. John McCarthy. 1962. Towards a Mathematical Science of Computation. In Proc. of IFIP 1962. 21\u201328."},{"key":"e_1_2_2_66_1","volume-title":"Braffort and D. Hirschberg (Eds.) (Studies in Logic and the Foundations of Mathematics","volume":"33","author":"McCarthy John","year":"1963","unstructured":"John McCarthy . 1963 . A Basis for a Mathematical Theory of Computation). In Computer Programming and Formal Systems, P . Braffort and D. Hirschberg (Eds.) (Studies in Logic and the Foundations of Mathematics , Vol. 35). Elsevier, 33 \u2013 70. John McCarthy. 1963. A Basis for a Mathematical Theory of Computation). In Computer Programming and Formal Systems, P. Braffort and D. Hirschberg (Eds.) (Studies in Logic and the Foundations of Mathematics, Vol. 35). Elsevier, 33 \u2013 70."},{"key":"e_1_2_2_67_1","volume-title":"Foundations for programming languages","author":"Mitchell John C.","unstructured":"John C. Mitchell . 1996. Foundations for programming languages . MIT Press . John C. Mitchell. 1996. Foundations for programming languages. MIT Press."},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_70_1","unstructured":"J. Morris. 1969. Lambda Calculus Models of Programming Languages. Ph. D. Dissertation. MIT. J. Morris. 1969. Lambda Calculus Models of Programming Languages. Ph. D. Dissertation. MIT."},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287580"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_2_73_1","volume-title":"Programming contextual computations. Ph. D. Dissertation","author":"Orchard Dominic A.","unstructured":"Dominic A. Orchard . 2014. Programming contextual computations. Ph. D. Dissertation . University of Cambridge , UK. Dominic A. Orchard. 2014. Programming contextual computations. Ph. D. Dissertation. University of Cambridge, UK."},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00028-3"},{"key":"e_1_2_2_78_1","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pitts A.M.","unstructured":"A.M. Pitts . 2011. Howe\u2019s Method for Higher-Order Languages . In Advanced Topics in Bisimulation and Coinduction , D. Sangiorgi and J. Rutten (Eds.) (Cambridge Tracts in Theoretical Computer Science, Vol . 52). Cambridge University Press , 197\u2013232. A.M. Pitts. 2011. Howe\u2019s Method for Higher-Order Languages. In Advanced Topics in Bisimulation and Coinduction, D. Sangiorgi and J. Rutten (Eds.) (Cambridge Tracts in Theoretical Computer Science, Vol. 52). Cambridge University Press, 197\u2013232."},{"key":"e_1_2_2_79_1","volume-title":"Semantics and Logics of Computation","author":"Pitts A. M.","unstructured":"A. M. Pitts . 1997. Operationally-Based Theories of Program Equivalence . In Semantics and Logics of Computation , P. Dybjer and A. M. Pitts (Eds.). Cambridge University Press , 241\u2013298. A. M. Pitts. 1997. Operationally-Based Theories of Program Equivalence. In Semantics and Logics of Computation, P. Dybjer and A. M. Pitts (Eds.). Cambridge University Press, 241\u2013298."},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_2_85_1","volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523","author":"Reynolds J.C.","year":"1983","unstructured":"J.C. Reynolds . 1983 . Types , Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523 . J.C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523."},{"key":"e_1_2_2_86_1","volume-title":"Meyer","author":"Routley Richard","year":"1973","unstructured":"Richard Routley and Robert K . Meyer . 1973 . The Semantics of Entailment. In Truth, Syntax and Modality, Hugues Leblanc (Ed.) (Studies in Logic and the Foundations of Mathematics , Vol. 68). Elsevier, 199 \u2013 243. Richard Routley and Robert K. Meyer. 1973. The Semantics of Entailment. In Truth, Syntax and Modality, Hugues Leblanc (Ed.) (Studies in Logic and the Foundations of Mathematics, Vol. 68). Elsevier, 199 \u2013 243."},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1042"},{"key":"e_1_2_2_88_1","unstructured":"M\u00edche\u00e1l \u00d3 Searc\u00f3id. 2006. Metric Spaces. Springer London. M\u00edche\u00e1l \u00d3 Searc\u00f3id. 2006. Metric Spaces. Springer London."},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_11"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363518"},{"key":"e_1_2_2_91_1","volume-title":"The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation","author":"Simpson Alex K.","unstructured":"Alex K. Simpson . 1994. The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation . University of Edinburgh , UK. Alex K. Simpson. 1994. The proof theory and semantics of intuitionistic modal logic. Ph. D. Dissertation. University of Edinburgh, UK."},{"key":"e_1_2_2_92_1","doi-asserted-by":"publisher","DOI":"10.2307\/2272559"},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498692","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498692","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498692"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":92,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498692"],"URL":"https:\/\/doi.org\/10.1145\/3498692","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}