Bialgebraic Reasoning on Higher-Order Program Equivalence
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911877742723072 |
|---|---|
| author | Goncharov, Sergey Milius, Stefan Tsampas, Stelios Urbat, Henning |
| author_facet | Goncharov, Sergey Milius, Stefan Tsampas, Stelios Urbat, Henning |
| contents | Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Our main result asserts that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and $λ$-calculi with recursive types, and to different flavours of contextual equivalence. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_00625 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Bialgebraic Reasoning on Higher-Order Program Equivalence Goncharov, Sergey Milius, Stefan Tsampas, Stelios Urbat, Henning Logic in Computer Science Programming Languages Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higher-order languages. Our main result asserts that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and $λ$-calculi with recursive types, and to different flavours of contextual equivalence. |
| title | Bialgebraic Reasoning on Higher-Order Program Equivalence |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2402.00625 |