Higher-Order Mathematical Operational Semantics (Early Ideas)

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

doi:10.4230/LIPIcs.CALCO.2023.24

Higher-Order Mathematical Operational Semantics (Early Ideas)

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

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Editors	Paolo Baldan, Valeria de Paiva
Publisher	Schloss Dagstuhl
Pages	24:1-24:3
ISBN (Electronic)	9783959772877
DOIs	https://doi.org/10.4230/LIPIcs.CALCO.2023.24
Publication status	Published - 2 Sept 2023
Externally published	Yes
Event	10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023 - Bloomington, United States Duration: 19 Jun 2023 → 21 Jun 2023

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	270
ISSN (Print)	1868-8969

Conference

Conference	10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023
Country/Territory	United States
City	Bloomington
Period	19/06/23 → 21/06/23

Bibliographical note

Publisher Copyright:
© Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat; licensed under Creative Commons License CC-BY 4.0.

Keywords

Abstract GSOS
applicative bisimilarity
bialgebra
lambda-calculus

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.CALCO.2023.24Licence: Creative Commons: Attribution (CC BY)

Cite this

Goncharov, S., Milius, S., Schröder, L., Tsampas, S., & Urbat, H. (2023). Higher-Order Mathematical Operational Semantics (Early Ideas). In P. Baldan, & V. de Paiva (Eds.), 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023) (pp. 24:1-24:3). Article 24 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 270). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.CALCO.2023.24

@inproceedings{2f27b407ac4c475c88e9c620ed081321,

title = "Higher-Order Mathematical Operational Semantics (Early Ideas)",

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.",

keywords = "Abstract GSOS, applicative bisimilarity, bialgebra, lambda-calculus",

author = "Sergey Goncharov and Stefan Milius and Lutz Schr{\"o}der and Stelios Tsampas and Henning Urbat",

note = "Publisher Copyright: {\textcopyright} Sergey Goncharov, Stefan Milius, Lutz Schr{\"o}der, Stelios Tsampas, and Henning Urbat; licensed under Creative Commons License CC-BY 4.0.; 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023 ; Conference date: 19-06-2023 Through 21-06-2023",

year = "2023",

month = sep,

day = "2",

doi = "10.4230/LIPIcs.CALCO.2023.24",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl",

pages = "24:1--24:3",

editor = "Paolo Baldan and \{de Paiva\}, Valeria",

booktitle = "10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)",

address = "Germany",

}

Goncharov, S, Milius, S, Schröder, L, Tsampas, S & Urbat, H 2023, Higher-Order Mathematical Operational Semantics (Early Ideas). in P Baldan & V de Paiva (eds), 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)., 24, Leibniz International Proceedings in Informatics, LIPIcs, vol. 270, Schloss Dagstuhl, pp. 24:1-24:3, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, Bloomington, United States, 19/06/23. https://doi.org/10.4230/LIPIcs.CALCO.2023.24

Higher-Order Mathematical Operational Semantics (Early Ideas). / Goncharov, Sergey; Milius, Stefan; Schröder, Lutz et al.
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). ed. / Paolo Baldan; Valeria de Paiva. Schloss Dagstuhl, 2023. p. 24:1-24:3 24 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 270).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Higher-Order Mathematical Operational Semantics (Early Ideas)

AU - Goncharov, Sergey

AU - Milius, Stefan

AU - Schröder, Lutz

AU - Tsampas, Stelios

AU - Urbat, Henning

N1 - Publisher Copyright: © Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat; licensed under Creative Commons License CC-BY 4.0.

PY - 2023/9/2

Y1 - 2023/9/2

N2 - 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.

AB - 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.

KW - Abstract GSOS

KW - applicative bisimilarity

KW - bialgebra

KW - lambda-calculus

UR - https://www.scopus.com/pages/publications/85172142327

U2 - 10.4230/LIPIcs.CALCO.2023.24

DO - 10.4230/LIPIcs.CALCO.2023.24

M3 - Conference contribution

AN - SCOPUS:85172142327

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 24:1-24:3

BT - 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

A2 - Baldan, Paolo

A2 - de Paiva, Valeria

PB - Schloss Dagstuhl

T2 - 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023

Y2 - 19 June 2023 through 21 June 2023

ER -

Higher-Order Mathematical Operational Semantics (Early Ideas)

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this