Abstract

A “type refinement system” is a type system built on top of a typed programming language, as an extra layer of typing. Type refinement systems in this sense have become increasingly popular in recent years as a lightweight mechanism for improving the correctness of programs. In the talk, I will give an introduction to a categorical perspective on type refinement systems that I have been developing over several years in collaboration with Paul-André Melliès, based on the simple idea of modelling a type refinement system as an “erasure” functor from a category of typing derivations to a category of terms. Some questions one can consider from this perspective include:

• What does it mean for a program to have more than one type? What does it mean for a typing judgment to have more than one derivation?

• How should we understand the so-called “subsumption rule” (a classical typing rule found in systems with subtyping)?

• If functors are type refinement systems, what does it mean for a functor to be a Grothendieck (bi)fibration?

A particular class of type refinement systems that are especially natural from this perspective are ones coming from a strict monoidal closed functor that is simultaneously a bifibration. I will give some examples illustrating how such type refinement systems can be used to give an axiomatic account of some phenomena from the semantics of separation logic and lambda calculus.