Complete trace models of state and control
<p>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.</p> <p>Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-ord...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2021
|
| _version_ | 1797074084306092032 |
|---|---|
| author | Jaber, G Murawski, AS |
| author_facet | Jaber, G Murawski, AS |
| author_sort | Jaber, G |
| collection | OXFORD |
| description | <p>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.</p>
<p>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.</p>
<p>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.</p> |
| first_indexed | 2024-03-06T23:31:12Z |
| format | Conference item |
| id | oxford-uuid:6c1503a0-0d8d-4a1e-90a8-3f1311ded403 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:31:12Z |
| publishDate | 2021 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:6c1503a0-0d8d-4a1e-90a8-3f1311ded4032022-03-26T19:08:29ZComplete trace models of state and controlConference itemhttp://purl.org/coar/resource_type/c_5794uuid:6c1503a0-0d8d-4a1e-90a8-3f1311ded403EnglishSymplectic ElementsSpringer2021Jaber, GMurawski, AS<p>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.</p> <p>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.</p> <p>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.</p> |
| spellingShingle | Jaber, G Murawski, AS Complete trace models of state and control |
| title | Complete trace models of state and control |
| title_full | Complete trace models of state and control |
| title_fullStr | Complete trace models of state and control |
| title_full_unstemmed | Complete trace models of state and control |
| title_short | Complete trace models of state and control |
| title_sort | complete trace models of state and control |
| work_keys_str_mv | AT jaberg completetracemodelsofstateandcontrol AT murawskias completetracemodelsofstateandcontrol |