Higher-Order Mathematical Operational Semantics (Early Ideas)

Goncharov, Sergey; Milius, Stefan; Schröder, Lutz; Tsampas, Stelios; Urbat, Henning

doi:10.4230/LIPIcs.CALCO.2023.24

File

LIPIcs.CALCO.2023.24.pdf

Filesize: 498 kB
3 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CALCO.2023.24
URN: urn:nbn:de:0030-drops-188213

Author Details

Sergey Goncharov

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Stefan Milius

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Lutz Schröder

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Stelios Tsampas

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Henning Urbat

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Cite AsGet BibTex

Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Higher-Order Mathematical Operational Semantics (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 24:1-24:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.24

Abstract

We present a higher-order extension of Turi and Plotkin’s abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe’s method is developed. It encompasses, for instance, Abramsky’s classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.

Subject Classification

ACM Subject Classification

Theory of computation → Categorical semantics

Keywords

Abstract GSOS
lambda-calculus
applicative bisimilarity
bialgebra

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

S. Abramsky. The lazy λ-calculus. In Research topics in Functional Programming, pages 65-117. Addison Wesley, 1990.
Filippo Bonchi, Daniela Petrişan, Damien Pous, and Jurriaan Rot. Lax bialgebras and up-to techniques for weak bisimulations. In CONCUR'15, pages 240-253, 2015.
Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In LICS'99, pages 193-202. IEEE, 1999.
Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In LICS'18, pages 452-461. ACM, 2018.
Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Towards a higher-order mathematical operational semantics. In POPL'23, volume 7, pages 632-658. ACM, 2023. URL: https://arxiv.org/abs/2210.13387.
Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In LICS'97, pages 280-291. IEEE, 1997.
Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, and Lutz Schröder. Weak similarity in higher-order mathematical operational semantics. In LICS'23. IEEE, 2023. URL: https://arxiv.org/abs/2302.08200.