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: Subject Reduction for Plus

If then Proof sketch:

Subject Reduction for Ite

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