[Seminar] Pragmatic Type and Effect Systems
Friday, February 28, 2025
11:00 am - 12:00 pm
Speaker
Edward
Lee
University
of
Waterloo
(Canada)
Location
PGH 232
Abstract
Type systems have long been used by humans to ensure that programs operate safely without unexpected behaviour. Historically they have done so by ensuring that operations are only passed in values they can handle; for example, ensuring that the function `add` is passed in exactly 2 integers. Recently however type systems have been enhanced to track, tame, and make safe other aspects of program behaviour, such as limiting where dangerous side effects can be performed and where objects can be mutated.
In my talk, I鈥檒l illustrate two recent pragmatic type systems for tracking said dangerous side effects. I鈥檒l point out how while on the surface these systems seem at all unrelated they share common algebraic properties that can be abstracted over and reused in other contexts as well. Finally, I鈥檒l wrap up by discussing potential avenues of future work, and how type systems remain relevant in an era where it isn鈥檛 just only humans writing the programs.
About the Speaker
Edward Lee is a PhD student in Computer Science at the University of Waterloo in Canada. He studies programming languages and types, with an eye to adding easy-to-use typing extensions to existing languages to make software safer. In a past life he used to study graph theory; nowadays he occasionally write formal, mechanized proofs for theorems about graphs.
