{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:23:50Z","timestamp":1787563430712,"version":"build-2736575974"},"reference-count":58,"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\/4.0\/"}],"funder":[{"name":"Royal Society University Research Fellow Enhancement Award","award":["RGF\/EA\/181059"],"award-info":[{"award-number":["RGF\/EA\/181059"]}]},{"name":"JST ERATO HASUO Metamathematics for Systems Design Project","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-1-0038"],"award-info":[{"award-number":["FA9550-21-1-0038"]}],"id":[{"id":"10.13039\/100000181","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>We present a construction which, under suitable assumptions, takes a model of Moggi\u2019s computational \u03bb-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, \u22a4\u22a4-lifting, and \u22a4\u22a4-closure, takes inspiration from O\u2019Hearn &amp; Riecke\u2019s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming.<\/jats:p>","DOI":"10.1145\/3498705","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T12:03:12Z","timestamp":1641988992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Fully abstract models for effectful \u03bb-calculi via category-theoretic logical relations"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-0929","authenticated-orcid":false,"given":"Ohad","family":"Kammar","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7529-5489","authenticated-orcid":false,"given":"Shin-ya","family":"Katsumata","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8320-0280","authenticated-orcid":false,"given":"Philip","family":"Saville","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.1998.705669"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275407"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_2_4_1","unstructured":"J. Adamek H. Herrlich and G.E. Strecker. 2009. Abstract and Concrete Categories: The Joy of Cats. Dover Publications. isbn:9780486469348 lccn:2009010561 https:\/\/books.google.co.jp\/books?id=rqT4PgAACAAJ  J. Adamek H. Herrlich and G.E. Strecker. 2009. Abstract and Concrete Categories: The Joy of Cats. Dover Publications. isbn:9780486469348 lccn:2009010561 https:\/\/books.google.co.jp\/books?id=rqT4PgAACAAJ"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00283-O"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511525858"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1047"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371131"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.011"},{"key":"e_1_2_2_10_1","volume-title":"Liguoro.","author":"U.","year":"1996","unstructured":"U. de \u2019 Liguoro. 1996 . PCF Definability via Kripke Logical Relations (after O\u2019Hearn and Riecke). Laboratoire d\u2019Informatique de l\u2019Ecole Normale Sup\u00e9rieure . U. de\u2019 Liguoro. 1996. PCF Definability via Kripke Logical Relations (after O\u2019Hearn and Riecke). Laboratoire d\u2019Informatique de l\u2019Ecole Normale Sup\u00e9rieure."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_2_12_1","first-page":"227","article-title":"Domains and denotational semantics: History, accomplishments and open problems","volume":"59","author":"Fiore M.","year":"1996","unstructured":"M. Fiore , A. Jung , E. Moggi , P. O\u2019Hearn , Riecke J., G. Rosolini , and I. Stark . 1996 . Domains and denotational semantics: History, accomplishments and open problems . Bulletin of EATCS , 59 (1996), 227 \u2013 256 . Edited by A. Jung. M. Fiore, A. Jung, E. Moggi, P. O\u2019Hearn, Riecke J., G. Rosolini, and I. Stark. 1996. Domains and denotational semantics: History, accomplishments and open problems. Bulletin of EATCS, 59 (1996), 227\u2013256. Edited by A. Jung.","journal-title":"Bulletin of EATCS"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS \u201999)","author":"Fiore M.","unstructured":"M. Fiore , G. Plotkin , and D. Turi . 1999. Abstract Syntax and Variable Binding . In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS \u201999) . IEEE Computer Society, Washington, DC, USA. 193\u2013. isbn:0-7695-0158-3 http:\/\/dl.acm.org\/citation.cfm?id=788021.788948 M. Fiore, G. Plotkin, and D. Turi. 1999. Abstract Syntax and Variable Binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS \u201999). IEEE Computer Society, Washington, DC, USA. 193\u2013. isbn:0-7695-0158-3 http:\/\/dl.acm.org\/citation.cfm?id=788021.788948"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"M. Fiore and A. Simpson. 1999. Lambda Definability with Sums via Grothendieck Logical Relations. In Typed Lambda Calculi and Applications J.-Y. Girard (Ed.). Springer Berlin Heidelberg Berlin Heidelberg. 147\u2013161. isbn:978-3-540-48959-7  M. Fiore and A. Simpson. 1999. Lambda Definability with Sums via Grothendieck Logical Relations. In Typed Lambda Calculi and Applications J.-Y. Girard (Ed.). Springer Berlin Heidelberg Berlin Heidelberg. 147\u2013161. isbn:978-3-540-48959-7","DOI":"10.1007\/3-540-48959-2_12"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0004972700044828"},{"key":"e_1_2_2_16_1","volume-title":"Proofs and types","author":"Girard J. Y.","year":"1810","unstructured":"J. Y. Girard . 1989. Proofs and types . Cambridge University Press , Cambridge . isbn:978052137 1810 J. Y. Girard. 1989. Proofs and types. Cambridge University Press, Cambridge. isbn:9780521371810"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0092872"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0960129508007172"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_31"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917)","author":"Heunen C.","unstructured":"C. Heunen , O. Kammar , S. Staton , and H. Yang . 2017. A Convenient Category for Higher-Order Probability Theory . In Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917) . IEEE Press, Article 77, 12 pages. isbn:9781509030187 C. Heunen, O. Kammar, S. Staton, and H. Yang. 2017. A Convenient Category for Higher-Order Probability Theory. In Proceedings of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201917). IEEE Press, Article 77, 12 pages. isbn:9781509030187"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_17"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_2_24_1","volume-title":"American Mathematical Society","author":"Iglesias-Zemmour P.","year":"1891","unstructured":"P. Iglesias-Zemmour . 2013. Diffeology. American Mathematical Society , Providence, Rhode Island. isbn :978082 1891 315 P. Iglesias-Zemmour. 2013. Diffeology. American Mathematical Society, Providence, Rhode Island. isbn:9780821891315"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-t"},{"key":"e_1_2_2_26_1","volume-title":"Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics). North Holland","author":"Jacobs B.","unstructured":"B. Jacobs . 1999. Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics). North Holland , Amsterdam . B. Jacobs. 1999. Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics). North Holland, Amsterdam."},{"key":"e_1_2_2_27_1","volume-title":"Sketches of an elephant : a topos theory compendium","author":"Johnstone P. T.","year":"1985","unstructured":"P. T. Johnstone . 2002. Sketches of an elephant : a topos theory compendium . Oxford University Press , Oxford New York. isbn:9780 1985 34259 P. T. Johnstone. 2002. Sketches of an elephant : a topos theory compendium. Oxford University Press, Oxford New York. isbn:9780198534259"},{"key":"e_1_2_2_28_1","unstructured":"A. Jung and J. Tiuryn. 1993. A new characterization of lambda definability. In Typed Lambda Calculi and Applications Marc Bezem and Jan Friso Groote (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 245\u2013257. isbn:978-3-540-47586-6  A. Jung and J. Tiuryn. 1993. A new characterization of lambda definability. In Typed Lambda Calculi and Applications Marc Bezem and Jan Friso Groote (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 245\u2013257. isbn:978-3-540-47586-6"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.11.012"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103698"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_8"},{"key":"e_1_2_2_33_1","volume-title":"A Characterisation of Lambda Definability with Sums Via \u22a4 \u22a4 -Closure Operators","author":"Katsumata S.","unstructured":"S. Katsumata . 2008. A Characterisation of Lambda Definability with Sums Via \u22a4 \u22a4 -Closure Operators . In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 278\u2013292. isbn:978-3-540-87531-4 S. Katsumata. 2008. A Characterisation of Lambda Definability with Sums Via \u22a4 \u22a4 -Closure Operators. In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 278\u2013292. isbn:978-3-540-87531-4"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.014"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01304852"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_17"},{"key":"e_1_2_2_37_1","unstructured":"F. W. Lawvere. 2006. Diagonal Arguments and Cartesian Closed Categories. Reprints in Theory and Applications of Categories 1\u201313. http:\/\/www.tac.mta.ca\/tac\/reprints\/articles\/15\/tr15.pdf  F. W. Lawvere. 2006. Diagonal Arguments and Cartesian Closed Categories. Reprints in Theory and Applications of Categories 1\u201313. http:\/\/www.tac.mta.ca\/tac\/reprints\/articles\/15\/tr15.pdf"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.exmath.2019.02.004"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55511-0_1"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/s1571-0661(05)80735-2"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.25"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56992-8_21"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_30"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1103"},{"key":"e_1_2_2_48_1","volume-title":"C-functors and C-morphisms. Publicationes mathematicae, 24, 3","author":"Pareigis B.","year":"1977","unstructured":"B. Pareigis . 1977. Non-additive ring and module theory II: C-categories , C-functors and C-morphisms. Publicationes mathematicae, 24, 3 ( 1977 ), January. B. Pareigis. 1977. Non-additive ring and module theory II: C-categories, C-functors and C-morphisms. Publicationes mathematicae, 24, 3 (1977), January."},{"key":"e_1_2_2_49_1","volume-title":"Lambda-definability and logical relations","author":"Plotkin G. D.","unstructured":"G. D. Plotkin . 1973. Lambda-definability and logical relations . University of Edinburgh. G. D. Plotkin. 1973. Lambda-definability and logical relations. University of Edinburgh."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_2_51_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Jonathan P","author":"Plotkin G. D.","unstructured":"G. D. Plotkin . 1980. Lambda-Definability in the Full Type Hierarchy . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Jonathan P . Seldin and J. Roger Hindley (Eds.). Academic Press . G. D. Plotkin. 1980. Lambda-Definability in the Full Type Hierarchy. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Jonathan P. Seldin and J. Roger Hindley (Eds.). Academic Press."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1023\/a:1023064908962"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_34"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.2957"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009901"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158148"},{"key":"e_1_2_2_57_1","volume-title":"Differential Geometrical Methods in Mathematical Physics","author":"Souriau J. M.","unstructured":"J. M. Souriau . 1980. Groupes differentiels . In Differential Geometrical Methods in Mathematical Physics , P. L. Garc\u00eda, A. P\u00e9rez-Rend\u00f3n, and J. M. Souriau (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg . 91\u2013128. isbn:978-3-540-38405-2 J. M. Souriau. 1980. Groupes differentiels. In Differential Geometrical Methods in Mathematical Physics, P. L. Garc\u00eda, A. P\u00e9rez-Rend\u00f3n, and J. M. Souriau (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 91\u2013128. isbn:978-3-540-38405-2"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90019-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498705","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498705","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498705","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:30:28Z","timestamp":1750174228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498705"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498705"],"URL":"https:\/\/doi.org\/10.1145\/3498705","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"}}]}}