Towards a Higher-Order Mathematical Operational Semantics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2022
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910196604862464 |
|---|---|
| author | Goncharov, Sergey Milius, Stefan Schröder, Lutz Tsampas, Stelios Urbat, Henning |
| author_facet | Goncharov, Sergey Milius, Stefan Schröder, Lutz Tsampas, Stelios Urbat, Henning |
| contents | Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2210_13387 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Towards a Higher-Order Mathematical Operational Semantics Goncharov, Sergey Milius, Stefan Schröder, Lutz Tsampas, Stelios Urbat, Henning Logic in Computer Science Programming Languages Category Theory Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. |
| title | Towards a Higher-Order Mathematical Operational Semantics |
| topic | Logic in Computer Science Programming Languages Category Theory |
| url | https://arxiv.org/abs/2210.13387 |