Operational algorithmic game semantics
We consider a simply-typed call-by-push-value calculus with state, and provide a fully abstract trace model via a labelled transition system (LTS) in the spirit of operational game semantics. By examining the shape of configurations and performing a series of natural optimisation steps based on name...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Association for Computing Machinery
2023
|
| _version_ | 1826310786194079744 |
|---|---|
| author | Bunting, B Murawski, AS |
| author_facet | Bunting, B Murawski, AS |
| author_sort | Bunting, B |
| collection | OXFORD |
| description | We consider a simply-typed call-by-push-value calculus with state, and provide a fully abstract trace model via a labelled transition system (LTS) in the spirit of operational game semantics. By examining the shape of configurations and performing a series of natural optimisation steps based on name recycling, we identify a fragment for which the LTS can be recast as a deterministic visibly pushdown automaton. This implies decidability of contextual equivalence for the fragment identified and solvability in exponential time for terms in canonical form. We also identify a fragment for which these automata are finite-state machines.Further, we use the trace model to prove that translations of prototypical call-by-name (IA) and call-by-value (RML) languages into our call-by-push-value language are fully abstract. This allows our decidability results to be seen as subsuming several results from the literature for IA and RML. We regard our operational approach as a simpler and more intuitive way of deriving such results. The techniques we rely on draw upon simple intuitions from operational semantics and the resultant automata retain operational style, capturing the dynamics of the underlying language. |
| first_indexed | 2024-03-07T07:57:07Z |
| format | Conference item |
| id | oxford-uuid:2cbf562f-33cc-4710-b32a-1df6a4477822 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T07:57:07Z |
| publishDate | 2023 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:2cbf562f-33cc-4710-b32a-1df6a44778222023-09-04T09:35:06ZOperational algorithmic game semanticsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:2cbf562f-33cc-4710-b32a-1df6a4477822EnglishSymplectic ElementsAssociation for Computing Machinery2023Bunting, BMurawski, ASWe consider a simply-typed call-by-push-value calculus with state, and provide a fully abstract trace model via a labelled transition system (LTS) in the spirit of operational game semantics. By examining the shape of configurations and performing a series of natural optimisation steps based on name recycling, we identify a fragment for which the LTS can be recast as a deterministic visibly pushdown automaton. This implies decidability of contextual equivalence for the fragment identified and solvability in exponential time for terms in canonical form. We also identify a fragment for which these automata are finite-state machines.Further, we use the trace model to prove that translations of prototypical call-by-name (IA) and call-by-value (RML) languages into our call-by-push-value language are fully abstract. This allows our decidability results to be seen as subsuming several results from the literature for IA and RML. We regard our operational approach as a simpler and more intuitive way of deriving such results. The techniques we rely on draw upon simple intuitions from operational semantics and the resultant automata retain operational style, capturing the dynamics of the underlying language. |
| spellingShingle | Bunting, B Murawski, AS Operational algorithmic game semantics |
| title | Operational algorithmic game semantics |
| title_full | Operational algorithmic game semantics |
| title_fullStr | Operational algorithmic game semantics |
| title_full_unstemmed | Operational algorithmic game semantics |
| title_short | Operational algorithmic game semantics |
| title_sort | operational algorithmic game semantics |
| work_keys_str_mv | AT buntingb operationalalgorithmicgamesemantics AT murawskias operationalalgorithmicgamesemantics |