剧情简介：An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. A program's type describes its behavior. Dependent types are a first-class part of a language, and are much more powerful than other kinds of types; using just one language for types and programs allows program descriptions to be as powerful as the programs they describe. The Littl...(展开全部)
作者：Daniel P. Friedman
出版社：MIT Press
ISBN：9780262536431
