Towards a Higher-Order Mathematical Operational Semantics
A talk by Sergey Goncharov
On Thursday 12th of January we will welcome Sergey Goncharov (FAU Erlangen-Nürnberg), for a talk at Reykjavik University. The talk will be given in room V105 at 16:00 and is a part of the ICE-TCS seminar at the Department of Computer Science.
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 has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far did not apply to higher-order languages. I will present a recently emerged 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 the present framework, the operational semantics of higher-order languages is represented by certain dinatural transformations, which we dub **higher-order GSOS laws**. I will present a general compositionality result w.r.t. a strong variant of Abramsky’s applicative bisimilarity that applies to all systems specified in this way, sticking to a variant of the combinatory logic, as a main vehicle. The talk is based on a recently accepted POPL'23 submission. This is a joint work with: Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat.
The talk will also stream on Zoom: https://eu01web.zoom.us/j/61692093974?pwd=T2NSSDZuYUF3cWZpcVNSZUNwb2xLUT09 Meeting ID: 616 9209 3974 Passcode: 608070
