Join us for a fascinating talk by Dr. Sergey Goncharov, Assistant Professor at the University of Birmingham, on bridging the gap between small-step and big-step operational semantics through abstract machinery. Discover how higher-order mathematical operational semantics unifies these foundational frameworks, and the ensuing Haskell implementation.

Title: From Small-Step to Big-Step, Abstractly

Speaker: Sergey Goncharov | University of Birmingham

When: 03/04(Tues) 11:00-12:00 (UTC+00:00)London

Where: Bayes Coffee House

External：https://app.huawei.com/wmeeting/join/96178839/RSJFvWSzybgEazWIJmZZOsfJ4izjWOmvY

Meeting ID: 96178839

Passcode: 932885

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS). Small-step semantics defines a fine-grained, one-step reduction relation on programs, while big-step semantics directly relates programs to their final evaluation results with respect to the ambient evaluation strategy. Although their agreement is critical for program analysis and reasoning, this is typically proven on a case-by-case basis, lacking a general theoretical foundation.

We address this by leveraging higher-order mathematical operational semantics — an abstract framework recently introduced as a generalization of its established first-order counterpart due to Turi and Plotkin.

Specifically, we introduce an abstract categorical notion of big-step SOS, complementing the existing (small-step) notion of abstract higher-order GSOS. We provide a general construction for deriving big-step semantics from small-step semantics, and prove an abstract equivalence between the two. The key construction for translating semantics from small-step to big-step is implemented in Haskell.

The talk is based on a joint work with Stelios Tsampas and Pouya Partow.

Bio: 

Dr. Sergey Goncharov is an Assistant Professor at the School of Computer Science, University of Birmingham. His research focuses on formal semantics of specification and programming languages, with the aim to abstract major idioms and unify diverse approaches for both theoretical and practical advancements. His interests encompass computational monads and side-effects, program logics, semantics and foundations of computation, universal (co)algebra, category theory, and hybrid systems.

His work on unifying notions of guarded fixed points earned him the EATCS Best Theory Paper Award 2018 (jointly with Lutz Schröder).

Prior to his recent appointment at the University of Birmingham, Dr. Goncharov has over years been a senior lecturer at the Chair for Theoretical Computer Science at FAU Erlangen-Nürnberg, Germany.

【BAYES COFFEE HOUSE TECH TALK SERIES】From Small-Step to Big-Step, Abstractly / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0