Notes on type theory and programming languages.