{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:52:40Z","timestamp":1770285160786,"version":"3.49.0"},"reference-count":53,"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":"DARPA and NIWC Pacific","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}]},{"name":"NSF","award":["2019285,1763399, 1521523, 2118851"],"award-info":[{"award-number":["2019285,1763399, 1521523, 2118851"]}]}],"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>Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state.<\/jats:p>\n          <jats:p>In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy's pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces.<\/jats:p>\n          <jats:p>After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces.<\/jats:p>","DOI":"10.1145\/3498703","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Layered and object-based game semantics"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1091-7560","authenticated-orcid":false,"given":"Arthur","family":"Oliveira Vale","sequence":"first","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6180-2275","authenticated-orcid":false,"given":"Paul-Andr\u00e9","family":"Melli\u00e8s","sequence":"additional","affiliation":[{"name":"CNRS, France \/ Universit\u00e9 de Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3168-5925","authenticated-orcid":false,"given":"J\u00e9r\u00e9mie","family":"Koenig","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4719-2922","authenticated-orcid":false,"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2015-2021. DeepSpec: The Science of Deep Specifications. https:\/\/deepspec.org\/  2015-2021. DeepSpec: The Science of Deep Specifications. https:\/\/deepspec.org\/"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3851-3_10"},{"key":"e_1_2_2_4_1","volume-title":"Game Semantics","author":"Abramsky Samson","unstructured":"Samson Abramsky and Guy McCusker . 1999. Game Semantics . In Computational Logic, Ulrich Berger and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 1\u201355. isbn:978-3-642-58622-4 Samson Abramsky and Guy McCusker. 1999. Game Semantics. In Computational Logic, Ulrich Berger and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201355. isbn:978-3-642-58622-4"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2016.0331"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90073-9"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.060"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.014"},{"key":"e_1_2_2_12_1","volume-title":"Parameterised Linearisability","author":"Cerone Andrea","unstructured":"Andrea Cerone , Alexey Gotsman , and Hongseok Yang . 2014. Parameterised Linearisability . In Automata, Languages, and Programming, Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 98\u2013109. isbn:978-3-662-43951-7 Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2014. Parameterised Linearisability. In Automata, Languages, and Programming, Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 98\u2013109. isbn:978-3-662-43951-7"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908100"},{"key":"e_1_2_2_17_1","volume-title":"Abstraction for Concurrent Objects","author":"Filipovi\u0107 Ivana","unstructured":"Ivana Filipovi\u0107 , Peter O\u2019Hearn , Noam Rinetzky , and Hongseok Yang . 2009. Abstraction for Concurrent Objects . In Programming Languages and Systems, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 252\u2013266. isbn:978-3-642-00590-9 Ivana Filipovi\u0107, Peter O\u2019Hearn, Noam Rinetzky, and Hongseok Yang. 2009. Abstraction for Concurrent Objects. In Programming Languages and Systems, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 252\u2013266. isbn:978-3-642-00590-9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.10.005"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916) . USENIX Association, USA. 653\u2013669. isbn:978 1931971331 Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916). USENIX Association, USA. 653\u2013669. isbn:9781931971331"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the Fourth International Conference on Applied Category Theory, Kohei Kishida (Ed.) (ACT","author":"Koenig J\u00e9r\u00e9mie","year":"2021","unstructured":"J\u00e9r\u00e9mie Koenig . 2021 . Grounding Game Semantics in Categorical Algebra . In Proceedings of the Fourth International Conference on Applied Category Theory, Kohei Kishida (Ed.) (ACT 2021). To appear. J\u00e9r\u00e9mie Koenig. 2021. Grounding Game Semantics in Categorical Algebra. In Proceedings of the Fourth International Conference on Applied Category Theory, Kohei Kishida (Ed.) (ACT 2021). To appear."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454097"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371088"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789814261456_0001"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209116"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394762"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676970"},{"key":"e_1_2_2_36_1","volume-title":"Interactive Models of Computation and Program Behaviour, Panoramas et Synth\u00e8ses 27. Soci\u00e9t\u00e9 Math\u00e9matique de France","author":"Melli\u00e8s Paul-Andr\u00e9","unstructured":"Paul-Andr\u00e9 Melli\u00e8s . 2009. Categorical Semantics of Linear Logic . In Interactive Models of Computation and Program Behaviour, Panoramas et Synth\u00e8ses 27. Soci\u00e9t\u00e9 Math\u00e9matique de France , Paris, France . 1\u2013196. Paul-Andr\u00e9 Melli\u00e8s. 2009. Categorical Semantics of Linear Logic. In Interactive Models of Computation and Program Behaviour, Panoramas et Synth\u00e8ses 27. Soci\u00e9t\u00e9 Math\u00e9matique de France, Paris, France. 1\u2013196."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535880"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.01.002"},{"key":"e_1_2_2_39_1","volume-title":"Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg","author":"O\u2019Hearn Peter W.","year":"2004","unstructured":"Peter W. O\u2019Hearn . 2004 . Resources , Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 49\u201367. isbn:978-3-540-28644-8 Peter W. O\u2019Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 49\u201367. isbn:978-3-540-28644-8"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00360-0"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Arthur Oliveira Vale Paul-Andr\u00e9 Melli\u00e8s Zhong Shao J\u00e9r\u00e9mie Koenig and L\u00e9o Stefanesco. 2021. Layered and Object-Based Game Semantics. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/layered.html  Arthur Oliveira Vale Paul-Andr\u00e9 Melli\u00e8s Zhong Shao J\u00e9r\u00e9mie Koenig and L\u00e9o Stefanesco. 2021. Layered and Object-Based Game Semantics. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/layered.html","DOI":"10.1145\/3498703"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316055"},{"key":"e_1_2_2_45_1","volume-title":"A Linear Logic Model of State. Dept. of Computer Science","author":"Reddy Uday S.","unstructured":"Uday S. Reddy . 1993. A Linear Logic Model of State. Dept. of Computer Science , UIUC , Urbana, IL . Uday S. Reddy. 1993. A Linear Logic Model of State. Dept. of Computer Science, UIUC, Urbana, IL."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01806032"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2927"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.020"},{"key":"e_1_2_2_49_1","volume-title":"Dunphy","author":"Reddy Uday S.","year":"2012","unstructured":"Uday S. Reddy and Brian P . Dunphy . 2012 . An Automata-Theoretic Model of Idealized Algol. In Automata, Languages, and Programming, Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 337\u2013350. isbn:978-3-642-31585-5 Uday S. Reddy and Brian P. Dunphy. 2012. An Automata-Theoretic Model of Idealized Algol. In Automata, Languages, and Programming, Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 337\u2013350. isbn:978-3-642-31585-5"},{"key":"e_1_2_2_50_1","volume-title":"Pomset logic: A non-commutative extension of classical linear logic","author":"Retor\u00e9 Christian","unstructured":"Christian Retor\u00e9 . 1997. Pomset logic: A non-commutative extension of classical linear logic . In Typed Lambda Calculi and Applications, Philippe de Groote and J. Roger Hindley (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 300\u2013318. isbn:978-3-540-68438-1 Christian Retor\u00e9. 1997. Pomset logic: A non-commutative extension of classical linear logic. In Typed Lambda Calculi and Applications, Philippe de Groote and J. Roger Hindley (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 300\u2013318. isbn:978-3-540-68438-1"},{"key":"e_1_2_2_51_1","doi-asserted-by":"crossref","unstructured":"Jerome H. Saltzer and M. Frans Kaashoek. 2009. Principles of Computer System Design. Morgan Kaufmann.  Jerome H. Saltzer and M. Frans Kaashoek. 2009. Principles of Computer System Design. Morgan Kaufmann.","DOI":"10.1016\/B978-0-12-374957-4.00010-4"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1859204.1859226"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360562"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498703","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498703","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498703","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\/3498703"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498703"],"URL":"https:\/\/doi.org\/10.1145\/3498703","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"}}]}}