Хороший небольшой обзор теории типов от Harley Eades. Подготовлен в 12-14 гг., область с тех пор ушла вперед, что, впрочем, не избавляет от необходимости знакомства с историей и состоянием области на (условный) вчерашний день.

https://metatheorem.org/includes/pubs/comp.pdf

Обзор был сделан в рамках подготовки к написанию диссертации, сама диссертация https://metatheorem.org/includes/pubs/thesis.pdf