Porgramming in Martin-Lof's Type Theory

Bengt Nordstrom, Kent Petersson, Jan M. Smith