This is a learning seminar on dependent type theory. We are currently following Peter Selinger's lecture notes on the lambda calculus (available online here: https://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf). This talk will cover chapter 9 of Selinger's notes, on algorithms for type checking and type inference in the simply typed lambda calculus.