Type Soundness for Simply Typed Lambda Calculus
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 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:
Subject Reduction for Plus
Subject Reduction for Ite
Subject Reduction for Beta Reduction Rule
Lemma: If and , then .
Note on Variable Capture