**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).

- Principles of Type Refinement: notes from a four-day lecture series on closely related topics at OPLSS 2016.

*Lambda Calculus with Types*by Barendregt, Dekkers, and Statman (CUP, 2013). Comprehensive reference on typing à la Curry, intersection types, and more, from a traditional ("syntactic") perspective.

- C. A. R. Hoare (1969), An Axiomatic Basis for Computer Programming
- Tim Freeman and Frank Pfenning (1991), Refinement Types for ML
- Rowan Davies and Frank Pfenning (2000), Intersection Types and Computational Effects
- John Reynolds (2000), The Meaning of Types: From Intrinsic to Extrinsic Semantics
- Harry Mairson (2002), Linear lambda calculus and PTIME-completeness
- Frank Pfenning (2008), Church and Curry: Combining Intrinsic and Extrinsic Typing
- Paul-André Melliès and Noam Zeilberger (2015), Functors are Type Refinement Systems
- Paul-André Melliès and Noam Zeilberger (2016), A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine