# Simple Types for Lambda Calculus

There are several type systems for lambda calculus

We consider here the simplest one

• types are disjoint
• only primitive and function types
• every lambda binding specifies its type

## Type Rules for Simply Typed Lambda Calculus

Environment maps variable names to types

### Example Primitive Operations

Among the primitive operations we consider

plus : int -> int -> int
ite  : bool -> int -> int

Example: if % denotes , type check lambda expression

(%f:int->int. (%x:int. f(f x))) (plus 8)

in environment