Higher-Order Mathematical Operational Semantics
<|reference_start|>Higher-Order Mathematical Operational Semantics: Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term \emph{(pointed) higher-order GSOS laws}. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the $\lambda$-calculus w.r.t.\ a strong variant of Abramsky's applicative bisimilarity are obtained as instances.<|reference_end|>
@article{goncharov2024higher-order,
    title={Higher-Order Mathematical Operational Semantics},
    author={Sergey Goncharov, Stefan Milius, Lutz Schr"oder, Stelios Tsampas,
  Henning Urbat},
    journal={arXiv preprint arXiv:2405.16708},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.16708},
    primaryClass={cs.LO cs.PL}
}