Contextual Types, Explained: Invited Tutorial

Contextual objects characterize an object M together with the typing context Ψ in which it is meaningful. This idea is then also internalized within the type theory itself using the notion of a contextual type which pairs the type A of an object together with the context Ψ in which the object is well-typed. In this tutorial, we review the origins of this idea and show its power in characterizing partial programs, mechanizing meta-theory, and meta-programming. Starting from the simply typed setting, we give an overview of existing work which adopts contextual types to dependent type theories and touch on future research directions.