Porgramming in Martin-Lof's Type Theory

Author — Bengt Nordstrom, Kent Petersson, Jan M. Smith