PGR Seminar – Leonid Nosovitskiy and Bhakti Shah
You are warmly invited to the next PGR Seminar.
Tuesday 24/02/2026
15:00-16:00
JC 1.33A
Speaker 1: Leonid Nosovitskiy
Title: Designing Interruptible Protocols in Distributed Systems
Abstract: Communication protocols are ubiquitous in distributed systems, and many are interruptible: they must handle optional, higher-priority events while a main interaction is in progress. Such protocols are used in systems such as finance (FIX), IoT (sensor-driven event protocols), and telecommunications (SIP). However, it is hard to model such protocols because they must coordinate mutually consistent behaviour across nodes in an asynchronous network. Variable interrupt delays can result participants to be in different global states, leading to unexpected behaviours, deadlocks, and potentially financial loss or denial of service. Even when an interrupt is successfully propagated, cohesively recovering to the pre-interrupt flow is often non-trivial. We address these challenges using Multiparty Session Types (MPST), which enable static verification of distributed protocol implementations for communication safety, liveness, and deadlock-freedom via high-level specifications and code-generation/type-checking toolchains. We extend the MPST specification language Scribble with a language-level abstraction for describing interruptible interactions. Our extension is encoded into existing Scribble constructs, preserving compatibility with current tooling while enabling cohesive, consistent specifications of interruptible protocols. The resulting approach supports interruptible protocol design while retaining node cohesiveness, and MPST guarantees of communication safety, liveness, and deadlock freedom.
Bio: Leonid Nosovitskiy is a PhD researcher working on Multiparty Session Types (MPST). His research focuses on refactoring and encoding techniques that enrich distributed-systems protocol specifications and their implementations, improving the usability of session-type tooling in more realistic settings and enabling verifiable, correct-by-construction protocol implementations.
Speaker 2: Bhakti Shah
Title: Imperative Syntax for Dependent Types
Abstract: The syntax of a functional, dependently typed programming language differs significantly from that of a typical imperative language. As a part of our goal to develop a dependent type theory and programming language tailored to imperative programmers, we wish to explore the impact of syntax on comprehensibility and usability of a dependently typed language, specifically for experienced imperative programmers. To this end, we develop a prototypical imperative syntax that can be transformed into an existing dependently typed language, Idris. We develop several transformation algorithms to take imperative constructs such as loops and statements from this syntax to terms that typecheck in Idris, allowing programs to be executed within Idris’s ecosystem. In particular, we establish a design pattern to take imperative-style code for finite state machines into executable, dependently typed programs that enforce type-level state constraints, using the established indexed monad pattern for state machines in dependently typed languages. We also develop an algorithm to automatically derive decidable equality instances for custom types, enabling dependent elimination with no additional effort from the programmer. As future work, we aim to conduct a formal user study to evaluate the effectiveness of this syntax for our purposes.
Bio: I am a second year PhD student supervised by Dr. Edwin Brady. My research relates to programming language theory and practice, specifically the design and implementation of usable dependently typed systems and languages.
We hope you can join us!