Computer Science PGR Seminar Leonid Nosovitskiy and Bhakti Shah

Leonid Nosovitskiy will present 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).

Bhakti Shah will present 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.

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.