Higher-Order Mathematical Operational Semantics
CALCO(2024)
Abstract
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 (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 λ-calculus
w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as
instances.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined