We introduce a number of typed lambda calculi, show how type theory may be used as basis for a proof assistant, and illustrate this with the Coq proof assistant.