Types and Programming Languages
第三章Untyped Arithmetic Expressions
Q: Why bother doing proofs about programming languages? They are almost always boring if the definitions are right.
A: The definitions are almost always wrong.
—Anonymous
第八章Typed Arithmetic Expressions
The road from untyped to typed universes has been followed many times, in many different fields, and largely for the same reasons.
—Luca Cardelli and Peter Wegner (1985)
最后一章
“Begin a