Radu Mardare

Radu Mardare  (Heriot-Watt University, Scotland)

Radu Mardare is a Professor at the School of Mathematics and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland. Prior to this, he was a Professor at University of Strathclyde (Glasgow, Scotland), at Aalborg University (Denmark), a researcher at the Microsoft Research CoSBi Centre (Italy) and at University of Trento (Italy). Mardare is an active researcher in the field of semantics where he advocates a combined used of logics, model theory and continuous mathematics.

Quantitative Algebraic Reasoning

This talk is meant to be a tutorial on the current research in the field of Quantitative Equational Logic and Quantitative Algebras. The intention is to cover the main concepts and constructions, the relevant examples, the varieties and quasivarieties theorems, as well as the extensions of the to fix-point theories. The talk will also describe recent directions and future challenges.

Simon Fowler

Simon Fowler  (University of Glasgow, Scotland)

Simon Fowler is a Lecturer in Programming Language Foundations at the University of Glasgow School of Computing Science. His research interests are in programming language design and implementation, with a particular focus on behavioural type systems and multi-tier programming. He is a co-investigator on the EPSRC-funded STARDUST project that investigates behavioural type systems for actor languages. Before joining Glasgow, he was a PhD student and subsequently postdoctoral researcher at the University of Edinburgh, and he has spent outside academia at IntelliFactory and OCaml Labs.

Mailbox Types: From Processes to Programming

Communication-centric programming languages like Go and Erlang sidestep many of the hazards of concurrent programming using shared state, but still remain vulnerable to errors like communication mismatches and deadlocks. Session types have gained popularity as a promising type discipline for channel-based languages. In contrast, actor languages like Erlang and Elixir have a substantially different communication model that supports many-to-one communication and where each actor has an incoming message queue known as a mailbox.

In 2018, de’ Liguoro and Padovani introduced a type discipline for mailboxes, and applied it to a minimal process calculus called the Mailbox Calculus. However, introducing mailbox typing to a programming language, as opposed to a process calculus, presents multiple challenges both for name hygiene and the design of a typechecker. I will discuss how we addressed these issues through the use of quasi-linear typing and a backwards bidirectional typing algorithm, as well as contrasting the connections between session types and automata with the connections between mailbox types and language inclusion problems in a commutative Kleene algebra.