Summary Introduction Preliminaries Proof Theory Category Theory Dependent Type Theory History Logical Relations Agda Coq NuPRL