Programming in Martin-Löf's Type Theory

by Bengt Nordström, Kent Petersson, Jan M. Smith