# Type Soundness for Simply Typed Lambda Calculus

We apply the general method in Proving Safety Properties using Types to prove soundness of Simple Types for Lambda Calculus

## Basic Notions

We consider the set of types given by these two rules:

- int, bool
- if , then also

(In particular types cannot have any 'variables' or 'parameters' as in more complex type systems.)

**Examples of types:** int, bool, int→bool, int→int, (int→bool)→bool, …

What is a configuration used to represent program execution?

What is the initial configuration?

What is the reduction relation ?

How to define the invariant ?

How can we define ?

- such that implies ?
- what kind of expressions will error denote?

## Well Typed Programs Have no Immediate Errors

## Evaluation Preserve Types: Subject Reduction

We next show that the invariant is inductive

What does this mean?

What does mean by Operational Semantics of Lambda with Letrec if we exclude rules for let/letrec

- primitive rule application in some context
- where denotes the constant

- beta reduction: