"Programming in Martin-Lof's Type Theory: An Introduction" - читать интересную книгу автора (Bengt Nordstrom, Kent Petersson, Jan M. Smith)