Conference item
Complete trace models of state and control
- Abstract:
-
We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either call/cc or no control operator.
Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and call/cc , constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively. This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or call/cc . Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively.
Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, 745.1KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-030-72019-3_13
Authors
- Publisher:
- Springer
- Host title:
- Programming Languages and Systems. ESOP 2021.
- Pages:
- 348-374
- Series:
- Lecture Notes in Computer Science
- Series number:
- 12648
- Publication date:
- 2021-03-23
- Acceptance date:
- 2020-12-20
- Event title:
- ESOP 2021: 30th European Symposium on Programming
- Event location:
- Online (Luxembourg)
- Event website:
- https://etaps.org/2021/esop
- Event start date:
- 2021-03-27
- Event end date:
- 2021-04-01
- DOI:
- ISSN:
-
0302-9743
- EISBN:
- 9783030720193
- ISBN:
- 9783030720186
- Language:
-
English
- Keywords:
- Pubs id:
-
1157758
- Local pid:
-
pubs:1157758
- Deposit date:
-
2021-01-22
Terms of use
- Copyright holder:
- Jaber and Murawski
- Copyright date:
- 2021
- Rights statement:
- © The Author(s) 2021. Open Access. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
- Notes:
- This paper was presented at ESOP 2021: 30th European Symposium on Programming, 27 March - 1 April 2021, Online (Luxembourg).
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record