# 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

We show that implies

Proof sketch:

## Evaluation Preserve Types: Subject Reduction

We next show that the invariant is inductive

What does this mean?

Given , can we guess what is?

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:

If

then

Proof sketch:

If

then

If

then

Proof sketch:

## Subject Reduction for Beta Reduction Rule

If

then

Proof sketch:

Lemma: If and , then .

Proof sketch:

Note on Variable Capture