Document Open Access Logo

Higher-Order Mathematical Operational Semantics (Early Ideas)

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2023.24.pdf
  • Filesize: 498 kB
  • 3 pages

Document Identifiers

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

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.

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

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

References

  1. S. Abramsky. The lazy λ-calculus. In Research topics in Functional Programming, pages 65-117. Addison Wesley, 1990. Google Scholar
  2. 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. Google Scholar
  3. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In LICS'99, pages 193-202. IEEE, 1999. Google Scholar
  4. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In LICS'18, pages 452-461. ACM, 2018. Google Scholar
  5. 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.
  6. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In LICS'97, pages 280-291. IEEE, 1997. Google Scholar
  7. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact