ThesisAuthors: Howse, Samuel (2006)
NummSquared Explained is the thesis version of the comprehensive formal docu¬ment NummSquared 2006a0 Done Formally, which is available at http / /nummist . com/poohbist/.
Set theory is the standard foundation for mathematics, but often does not include rules of reduction for function calls. Therefore, for computer science, the untyped lambda calculus or type theory is usually preferred. The untyped lambda calculus (and several improvements on it) make functions fundamental, but suffer from non-terminating reductions and have partially non-classical logics. Type theory is a good foundation for logic, mathematics and computer science, except that, by making both types and functions fundamental, it is more complex than either set theory or the un¬typed lambda calculus. This document p... 
