LIPIcs.CALCO.2023.24.pdf
- Filesize: 498 kB
- 3 pages
Document
Higher-Order Mathematical Operational Semantics (Early Ideas)
Authors
Sergey Goncharov 
,
Stefan Milius ,
Lutz Schröder ,
Stelios Tsampas ,
Henning Urbat
-
Part of:
Volume:
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-02
File
Document Identifiers
Author Details
Cite As Get 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)
0PDF Downloads
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.