Posts tagged with "type theory"

Large

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.

Large

Types and Type Theory

August 3rd, 2009

Programmers are all familiar with types.
Usually, their first experience with types comes from variable declarations in a language like Java or C, which look like the examples in (1).

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