##The simply-typed lambda calculus##
-The uptyped lambda calculus is pure computation. It is much more
+The untyped lambda calculus is pure computation. It is much more
common, however, for practical programming languages to be typed.
Likewise, systems used to investigate philosophical or linguistic
issues are almost always typed. Types will help us reason about our