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: