Sábháilte in:
| Príomhchruthaitheoirí: | , , , , |
|---|---|
| Formáid: | Preprint |
| Foilsithe / Cruthaithe: |
2024
|
| Ábhair: | |
| Rochtain ar líne: | https://arxiv.org/abs/2405.16708 |
| Clibeanna: |
Cuir clib leis
Níl clibeanna ann, Bí ar an gcéad duine le clib a chur leis an taifead seo!
|
| _version_ | 1866917547872354304 |
|---|---|
| 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 provides 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 combinatory logics and the lambda-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_16708 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Higher-order bialgebraic semantics Goncharov, Sergey Milius, Stefan Schröder, Lutz Tsampas, Stelios Urbat, Henning Logic in Computer Science Programming Languages 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 provides 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 combinatory logics and the lambda-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. |
| title | Higher-order bialgebraic semantics |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2405.16708 |