Types and Type Theory (part 2)

August 24th, 2009

In my previous post I mentioned different ways in which programming languages (and programmers) make use of types and type theory. In my next post I would like to describe the formal system which underlies almost all typed programming languages, the “simply-typed lambda calculus.” But before I get to that, I need to explain the (untyped) lambda calculus, its history, motivation, and functionality.

This is Part 2 in a multi-part series on the subject of Types and Type Theory.