## Simply Typed Lambda Calculus

###### 10/15/19

## DRAFT

## Introduction

The Lambda Calculus that we have been looking at thus far 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.