Type theory series: Untyped Lambda Calculus, Simply Typed Lambda Calculus, Fun with Curry-Howard, Polymorphism (System F), Dependent Types

A five-part series of talks introducing type theory at the SF Types, Theorems and Programming Languages meetup, working up from the untyped lambda calculus through System F to dependent types.