Introduction to Higher-Order Mathematical Operational Semantics

Abstract: Reasoning about program equivalence in higher-order setting is one of the central topics in computer science, with the classical lambda-calculus as a prototypical example and with its countless flavors and extensions thereof, all the way up to Haskell and OCaml. A recently emerged program of higher-order mathematical operational semantics aims to abstract and unify reasoning methods for such languages on the basis of two parameters: the language syntax and its (small-step) operational semantics. Thus, higher-order mathematical operational semantics is a natural extension of the pioneering Turi and Plotkin's (first-order) mathematical operational semantics. Our program takes its origin from a joint POPL-2023 publication with Stelios Tsampas, Henning Urbat, Stefan Milius, and Lutz Schröder, on which my present talk is largely based. Additionally, I will survey, more succinctly, subsequent advances of this program, outline challenges and perspectives for further work.

logic in computer scienceprogramming languagescomputer science theorycategory theorylogic

Audience: researchers in the topic

University of Birmingham theoretical computer science seminar

Series comments: Meeting ID: 818 7333 5084 ~ Password: 217