Martin Lof's type theory is a dependent type theory, used in formal proofs (e.g. Agda).
Main material: http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
Additional material: https://www.dimap.ufrn.br/~regivan/pub/Programming_In_Martin_Loef_Type_Theory.pdf
MLTT 中最核心的概念是 Proof。