Type Refinement Systems

Advanced course for MGS 2019

Noam Zeilberger (University of Birmingham)

Abstract A type refinement system is, roughly speaking, a type system built on top of a language that is already typed, as an extra layer of typing. Type refinement systems in this (admittedly very broad!) sense have become popular in recent years as a lightweight approach to improving program correctness. The course will focus on the theoretical foundations of type refinement, taking as a guiding principle the naive idea of viewing type refinement systems categorically as "forgetful" functors from a category of typing derivations to a category of terms. After reviewing this basic idea, we will consider a few idealized type refinement systems to familiarize ourselves with concepts such as subtyping, intersection types, bidirectional typing, and principality. Then we will continue to explore the implications of the functorial view, studying how it can be used to analyze the syntax and semantics of type refinement systems within an axiomatic framework, and conversely, using the perspective of type refinement as a source of new intuitions for some classical constructions in category theory (such as the Grothendieck construction).

Prerequisites some basic familiarity with simply typed lambda calculus and with a few elementary definitions from category theory (functors, cartesian closed categories and/or symmetric monoidal closed categories, adjunctions).

Lecture notes

Exercises

Other background material

Textbooks Articles