Higher-Order Mathematical Operational Semantics - From Abstract GSOS to Compositionality

Explore a one-hour Topos Institute Colloquium lecture that delves into the development of higher-order GSOS specifications for programming languages. Learn how compositionality proofs in higher-order languages can be approached through dinatural transformations, known as higher-order GSOS laws. Discover how Turi and Plotkin's bialgebraic abstract GSOS framework, traditionally used for first-order languages, has been adapted for higher-order applications. Examine a general compositionality result related to Abramsky's applicative bisimilarity, demonstrated through combinatory logic examples. Progress through key concepts including First Order GSS, Operational Semantics, Higher-Order GSS, Operational Models, Congruence, Algebraic morphisms, and Bio algebras. Based on research presented at POPL'23 by Sergey Goncharov in collaboration with Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat.