## Lambda Calculus with Elementary Type Theory

###### 8/23/21

The Lambda Calculus that we have been looking at in Lambda Calculus and Combinatory Logic has been the *untyped* Lambda Calculus. It is plenty interesting for sure, being able to provide a foundation for computability, programming languages, and many areas of linguistics and philosophy. But untyped Lambda calculus also has some features to be wary of; for example, some reduction sequences go on forever and never reduce the expression to a normal form.