My Notes for UCLA CS231: Types and Programming Languages

This is my notes for CS231 Types and Programming Languages during Winter 2021 at UCLA. I find this class extremely interesting and want to share my notes for people are/will be taking the course as a reference, and for those considering taking the course to see what the content is like. If you are an UCLA student considering taking this course, I am happy to answer any questions and talk about the class with you.

Quick FAQ:

• What is the course about?
  • This course is about the theory of type checking. The core goal of the class is to show you how type checking guarantees runtime “correctness”. In the course, you will get to construct an OCaml-like language from ground up by adding features (variables, functions, tuples, unions) one at a time. While adding each feature, we use maths to prove that our type system will guarantee that the feature will run correctly at runtime. Towards the end of the course, we get to use an automatic theorem prover called Coq.
• How are the assignments and exams?
  • Since the course is about proving that type checking works, you will be writing some proofs in the homework. You will also write some OCaml code. (Don’t be scared, the OCaml code assignment is not like 131.) The exam is very similar style to the homework. If you can handle the homework, you can handle the exam.
• If I am an undergrad, can I take this course?
  • Yes! I took this course as an undergrad. Check with the department for the process to enroll in grad classes as undergrad.
• What are some background knowledge that helped in 231?
  • The course enforces CS 131 as a pre-requisite. You need to know some basic OCaml for the coding homework, and having some basic understanding of the OCaml type constructs like tuple, unions, pattern matching, and functions definitely helps. I also took CS 132 (compiler construction) before 231, which helped me gain some experience of writing code for type checking. But I will say 132 is nice to have but not necessary. Knowing how to write LaTeX helped with the homework.

Table of Contents for Notes:

• Operational Semantics
  • Big-step operational semantics
    • Applying inference rule
    • Plus
    • Greater
  • Proving properties given rules
    • Structural induction
  • Small-step operation semantics
    • Some terminology related to small-step semantics
  • Practicing Proof
• Static Type System
  • Type Soundness
    • Progress + Preservation
• Lambda Calculus
  • untyped lambda calculus (chapter 5)
    • Omega term
  • Congruence rule
    • Call-by-value
    • Church Booleans
    • Church numerals
  • Simply-Typed Lambda Calculus
    • Typecheck variable
    • Typecheck function
    • Typecheck function call
• Logic and typechecking
  • Curry-Howard Isomorphism
  • Logical Conjunction in type system
  • Logical Disjunction
  • Type True
• Adding features
  • Local Variables
  • Sequencing (side-effect)
  • Recursion
• Type Inference
  • Constraint Generation
    • Correctness of Constraint Generation
  • Constraints Solving
  • Polymorphic Lambda Calculus (System F, Second-Order Lambda Calculus)
    • Example: swap
    • Operational semantics for polymorphic lambda
    • Typecheck for polymorphic lambda
  • Existential quantification
• Proof assistant
  • Defining boolean
  • Defining negate
  • Running computation:
  • Writing a lemma
  • Proofing the lemma
  • Defining list
  • Defining Recursion
  • Proof by Induction
  • Parametric polymorphism
  • Defining Pairs
  • Dependent Proposition
  • Proofs of 231 in Coq
    • Typechecking
    • Small-step operational semantics
    • Proving Progress and Preservation
• Mutable References
  • Typing rules
  • Small-step semantics
  • Type Soundness with reference
  • Typing rule of location
• Subtyping
• Type and Effect Systems
  • Monads

Operational Semantics

Big-step operational semantics

The simple language that we are working with today defined in BNF grammar:

t ::= true | false | if t then t else t

The language gives some results. We call these values and they can be defined as grammar as well.

v ::= true | false

P.S. for this class. Values are usually a subset of the grammar.

We first define a interpreter for this language.

(* the types to represent the tree *)
type t = True | False | If of t * t * t
(* 
 * How to initialize If:
 *   If (True, False, True)
 *)

(* the values/outputs of the program *)
type v = TrueV | FalseV

An interpreter at this point is a function that takes a term of type t and return a value of type v.

let rec eval (t:t):v = 
    match t with 
        True -> TrueV
    |   False -> FalseV
    |   If(cond, thn, els) ->
        match eval cond with
            TrueV -> eval thn
        |   FalseV -> eval els

So, big-step operation semantics really means we define a function that takes in a term to produce a value. This relationship is the big step operation semantics. Notation: $t \Downarrow v$ (read as $t$ big-steps to $v$)

In world of logic: binary relation, predicate, logical judgement.

Big-step operational semantics give rules to define the relation. Notation of a rule:

We attempt to writes the rules for the simple language defined above.

The rule $E_{val}$ has no premises. It is called an axiom. The logical equivalence of this rule is:

Now we consider a rule where If condition evals to true.

Logical equivalence

We can define the rule for false.

Applying inference rule

Claim: if true then false else true $\Downarrow$ false

We pick a rule to apply to the claim. We appeal to $E_{IfTrue}$. Then we recursively prove each preconditions.

This is a derivation tree. To know the tree is correct. We can simply apply the rules and see if the correct predicates are evaluated. So a simple process.

If we choose the wrong rule initially. Our proof cannot proceed. A derivation attempt that fails:

Goal: if true then (if false then true else false) else true $\Downarrow$ false

Now we make our language more interesting by adding numbers.

t ::= true | false | if t then t else t 
     | n | t + t | t > t
n ::= <integer constants>

We manipulate the interpreter.

type t = True | False | If of t * t * t
        | Int of int | Plus of t * t | Greater of t * t

type v = TrueV | FalseV | IntV of int

let rec eval (t:t):v = 
    match t with 
        True -> TrueV

    |   False -> FalseV

    |   If(cond, thn, els) ->
        match eval cond with
            TrueV -> eval thn
        |   FalseV -> eval els

    |   Int i -> IntV i

    |   Plus (t1, t2) -> 
        (match (eval t1, eval t2) with -> 
            (Intv i, IntV j) -> IntV (i+j))

    |   Greater(t1, t2) -> 
        (match (eval t1, eval t2) with -> 
            (IntV i, IntV j) -> 
                if i > j then TrueV else FalseV)

When Plus evals does not match two ints, OCaml throws a runtime error. To

be nicer, we add a Exception match clause

_ -> raise TypeError

This is dynamically typed language. If we don’t encounter type error during execution, we don’t do anything. For instance, an if-expression:

if true then true else false + 1

since the else-branch is never evaluated, we don’t care about the type mismatch there. We continue from last time. Let’s write out the rule for Plus and Greater than.

Plus

• Note that $[[+]]$ means a mathematical plus

Greater

We introduce another metavariable for type of value for boolean.

t ::= b | if t then t else t
    | n | t + t | t > t
b ::= true | false
n ::= integer constants
v ::= b | n

Proving properties given rules

Let’s go back to the simplistic OCaml with only boolean without the integer values.

Theorem: For all terms t, there exists value v such that t $\Downarrow$ v.

Note this theorem might not be true for turing complete languages. The term might get stuck in infinite loop.

There is infinite number of terms. We use induction to prove it.

Structural induction

We want to prove $P(t)$ for all terms $t$.

• Prove $P(t)$ for separately for each kind of term
  • we can assume that $P(t')$ holds for each subterm $t'$ in $t$

Proof: by structural induction on $t$.

• Induction hypothesis: for all terms $t'$ such that $t'$ is a subterm of $t$,

there exists value $v'$ such that $t' \Downarrow v'$.

• Case analysis on the root node in $t$.
  • Case $t$=true: By $E_{val}$, $true \Downarrow true$.
  • Case $t$=false: By $E_{val}$, $false \Downarrow false$.
  • Case $t$ = if t1 then t2 else t3:
    • By induction hypothesis on $t_1$, there exists $v_1$ such that $t_1$ $\Downarrow$ $v_1$.
      • Case $v_1$=true: By IH on $t_2$, there exists $v_2$ such that $t_2 \Downarrow v_2$.
        • Then by $E_{IfTrue}$ if t1 then t2 else t3 $\Downarrow v_2$
      • Case $v_1$=false: By IH on $t_2$, there exists $v_3$ such that $t_3 \Downarrow v_3$.
        • Then by $E_{IfFalse}$ if t1 then t2 else t3 $\Downarrow v_3$
• QED

You can only do a case analysis on something that you know to exists/be true.

Example: for the same theorem, we cannot do a case analysis on $v$. Since the goal is to prove $v$ exists, to do a case analysis we are just saying that $v$ exists.

Small-step operation semantics

Judgement of form $t\rightarrow t'$, meaning $t$ evaluates in one step to $t'$. It is a single step of derivation. What is a single step of derivation?

Example:

if (if true then false else true) then false else true 

(* single-step to --> *)

if false then false else true 

(* single-step to --> *)

true

Two types of small-step rules:

• “computation” rules that simply do one small bit of evaluation
• “congruence” rules that simply tell you where to look recursively for the next bit of work

Examples of computation rule:

Well, not all if statements simply uses true or false as the condition. We need a congruence rule to tell us what to do

• from this congruence rule, we ended up with a new piece of program.
• a derivation tree here is simply a derivation list.

An example of derivation:

Plus rules

• Red stands for reduction

• Notice that we have taken explicit control over the order of evaluation: always left term first

• notice that we didn’t enforce the type of $v1$ since, we only enforce the

requirement at the moment of addition (aka $E_{PlusRed}$). This is nice since the operands can be different types and it is useful to put constraints only when it is absolutely needed.

Some terminology related to small-step semantics

A term $t$ is called a normal form if there does not exist a $t'$ such that $t \rightarrow t'$.

• example: true
• in general, we will arrange it such that values are normal forms

There are normal forms that are not values.

• example: true + 5

A normal form that is not a value is called a stuck expression

• run-time type error

Stuck expression can be arbitrarily large.

• That means you cannot take a step to get a smaller program
• (true) + 5 is stuck
• if (true + 5) then 0 else 1 is stuck
• if (if (true + 5) then 0 else 1) then 0 else 1 is stuck

Define a second judgement that is simply reflexive, transitive closure of the $\rightarrow$ relation. “Multi-step relation” notated as $t\rightarrow^* t'$.

Now we can derive the execution of the entire program using this relation in a single tree just as in big-step semantics.

Definition: a term is eventually stuck if $t \rightarrow^* t'$ and $t'$ is stuck.

(true + 5) is eventually stuck

• in general, all stuck expressions are also eventually stuck.

Example of eventually stuck: if true then (5 + true) else 0

• note that this expression is not stuck. We can still take a step to reduce it to 5 + true
  • if true then (5 + true) else 0 $\rightarrow$ 5 + true
• note that if (5 + true) then 1 else 0 is stuck tho. Since we cannot take an step to reduce it

What is this in a real programming language?

• a bad program
• a program that will eventually crash

Practicing Proof

Define the $falseCount$ of a term $t$ as follows:

• $falseCount(true) = 0$
• $falseCount(false) = 1$
• $falseCount(\text{if t1 then t2 else t3}) = falseCount(t1) + falseCount(t2) + falseCount(t3)$

We are given a lemma $FC_{Nonneg}$: for all $t$, $falseCount(t) \geq 0$.

Theorem: If $t \longrightarrow t'$, then $falseCount(t') \leq falseCount(t)$.

Proof: we perform a structural induction on $t$.

• induction hypothesis: For all subterm $t'$ of $t$, if $t' \rightarrow t''$, $falseCount(t'') \leq falseCount(t')$

We can do case analysis on root node term $t$. An alternative, when we are given a derivation ($t\rightarrow t'$), is to do case analysis on the rules.

Case analysis on the root rule in the derivation of $t\rightarrow t'$:

• Case $E_{IfTrue}$: Then $t = \texttt{if true then t2 else t3 }$ and $t’ =

t2$.

• By definition of $falseCount(t)= falseCount(t2) + falseCount(t3)$.
• By $FC_{Nonneg}$, $falseCount(t2) \geq 0$ and $falseCount(t3) \geq 0$.
• Therefore, $falseCount(t2) + falseCount(t3) \geq falseCount(t2)$
• Case $E_{IfFalse}$, same idea as above
• Case $E_{If}$, Then $t=\texttt{if t1 then t2 else t3}$ and $t'=\texttt{if t1' then t2 else t3}$ and $t1\rightarrow t1'$.
  • By IH, $falseCount(t1') \leq falseCount(t1)$
  • Therefore, $falseCount(t1') + falseCount(t2) + falseCount(t3) \leq falseCount(t1) + falseCount(t2) + falseCount(t3)$.
  • THen, the result follows from the definition of $falseCount$.

If we were to perform a case analysis, we also have to cover cases where term is true and we need to say that there is no derivation possible by deriving a contradiction, very annoying.

Note: this theorem does not hold when we add integer into the language. Since we can derive false from 0 > 1.

Exercise: proving lemma $FC_{Nonneg}$:

• By structural induction on $t$.
• IH: for all $t'$ which is a subterm of $t$, $falseCount(t') \geq 0$
• Case $t=true$, $falseCount(t) = 0 \geq 0$
• Case $t=false$, $falseCount(t) = 1 \geq 0$
• Case $t=\texttt{if t1 then t2 else t3}$
  • By IH, $falseCount(t1) \geq 0$,$falseCount(t2) \geq 0$, $falseCount(t3) \geq 0$
  • By def of $falseCount$, $falseCount(t) \geq 0$

Now that we have the proof, we name it lemma $FC_{Step}$. Next, we derive the theorem for multi-step.

Theorem: if $t \rightarrow^* t'$, then $falseCount(t') \leq falseCount(t)$.

Proof: By structural induction on $t$,

• IH: If $t0 \rightarrow^* t0'$, where $t0$ is a subterm of $t$, then $falseCount(t0') \leq falseCount(t0)$.
• Case analysis on the root rule in the derivation of $t \rightarrow^* t'$
  • Case $M_{Refl}$: Then $t=t'$, then $falseCount(t') = falseCount(t) \leq falseCount(t)$.
  • Case $M_{Step}$, Then $t\rightarrow t'$, By $FC_{Step}$, $falseCount(t') \leq falseCount(t)$.
  • Case $M_{transitive}$, then $t\rightarrow^* t''$ and $t'' \rightarrow^* t'$.
    • $\textbf{WE ARE STUCK}$

We cannot use our induction hypothesis here. There is no valid subterm relationship. There is no subterm we can grab for the transitive relationship.

Solution: we don’t do structural induction on $t$. Instead we do a induction on the derivation tree.

We restart our proof. First, rewrite the theorem such that our derivation is given a name.

Theorem: If $d: t\rightarrow^* t'$, then $falseCount(t') \leq falseCount(t)$.

Proof: By structural induction on $d$, which is the derivation of $t \rightarrow^* t'$

• IH: If $d_0: t_0 \rightarrow t_0'$, where $d_0$ is a subderivation of $d$,

then $falseCount(t_0')\leq falseCount(t_0)$.

• Case analysis on the root rule in the derivation of $t \rightarrow^* t'$:
  • Case $M_{Refl}$: Then $t=t'$, then $falseCount(t') = falseCount(t) \leq falseCount(t)$.
  • Case $M_{Step}$: Then $t\rightarrow t'$, By $FC_{Step}$, $falseCount(t') \leq falseCount(t)$.
  • Case $M_{Transitive}$: Then $d_1: t\rightarrow^* t''$ and $d_2: t''\rightarrow^* t'$.
    • By IH on $d_1$, $falseCount(t'') \leq falseCount(t)$
    • By IH on $d_2$, $falseCount(t') \leq falseCount(t'')$
    • Therefore, result follows by transitivity.

We can do this since derivation tree is a tree. It is recursively defined so we can perform structural induction as well.

Take home: we can apply this type of induction on the $FC_{Step}$

Theorem: If $d: t \rightarrow^* t'$ and $t \neq t'$, then there exists a $t''$ such that $t\rightarrow t''$ and $t'' \rightarrow^* t'$.

Proof: by structural induction on $d$.

• IH: If $d_0: t_0 \rightarrow^* t_0'$ and $t_0 \neq t_0'$ and $d_0$ is a subderivation of $d$, then there exists a $t_0''$

such that $t_0\rightarrow t_0''$ and $t_0'' \rightarrow^* t_0'$.

• Case analysis on the root rule in the derivation of $t \rightarrow^* t'$:
  • Case $M_{Refl}$: Then $t = t'$. This is a contradiction. This case is not part of the theorem.
  • Case $M_{Step}$: Then $t \rightarrow t'$
    • by $M_{Refl}$, $t' \rightarrow^* t'$
    • Therefore, $t\rightarrow t'$ and $t' \rightarrow^* t'$
  • Case $M_{Transitive}$: Then $d_1: t\rightarrow^* t_0$ and $d_2: t_0\rightarrow^* t'$.
    • Case analysis on the relationship between $t$ and $t_0$:

    • This case analysis is to satisfy IH condition $t \neq t'$. So that we mathematically satisfies the IH.

      • Case $t \neq t_0$:
        • By IH on $d_1$, $t\rightarrow t_n$ and $t_n \rightarrow^* t_0$.
        • Therefore, $t\rightarrow t_n$ and $t_n \rightarrow^* t_0$ and $t_0 \rightarrow^* t'$
        • By $M_{Transitive}$, $t\rightarrow t_n$ and $t_n \rightarrow^* t'$.
        • result follows $t'' = t_0$.
      • Case $t = t_0$:
        • Case analysis on the relationship between $t_0$ and $t'$:
          • Case $t_0 \neq t'$: By IH, there exists $t_n$ such that $t_0 \rightarrow t_n$ and $t_n \rightarrow^* t'$. Since $t=t_0$, the result follows with $t'' = t_n$.
          • Case $t_0 = t'$. Then $t = t'$. Contradiction.

Wow, a deeply nested structural induction. We have 3 levels of case analysis nested inside each other.

Static Type System

textbook: Chapter 8

Goal: Get rid of type error at compile time.

Previously, we have big-step, small-step and multi-step semantics judgement form. We need a new judgement form.

To build a type system, we assign each expression a type.

T ::= Bool | Int

The new typing judgement of the form $t: T$, which means “term $t$ has type $T$.

Note that we don’t have value evaluation here. But we have type assignment.

We can build derivation tree from these rules again.

We can have derivation that doesn’t work.

Rule for Greater

Rule for If

• we are forcing the true branch and false branch to have the same type
• figuring out eventually stuck expression is undecidable. A sound type system always be conservative and rule out program that technically run fine.

  if true then 0 else false

  This will evaluate to 0. But OCaml will prevent it from even running.

What if we want if true then 0 else false to pass the type check? We can add If-True rule.

$$\cfrac{ t2: T }{ \texttt{if true then t2 else t3}: T }\quad {T_{IfTrue}}$$

However, this rule is very limited since it requires the if to have syntactically have true as condition. Oh Bad.

We also cannot statically know what the condition will be, even we introduce a true or false type. So we like forcing if statement to have the same type.

Example: Build a type derivation tree

for if 3 > 2 then 0 else 1+2 build a derivation tree.

Type Soundness

How to we prove that our type system has eliminated type error before runtime?

“Well-typed programs don’t go wrong” (Milner)

Our goal: Well-typed programs are not eventually stuck.

Theorem (Type Soundness)

• attempt 1: If $t : T$, then either $t$ is a value or exists $t'$ s.t. $t \rightarrow^* t'$.
  • this is not what we want. According to multi-step semantics. Any stuck expression multi-step to itself.
• attempt 2: If $t : T$, then either $t$ is a value or exists $t'$ s.t. $t \rightarrow t'$.
  • Not good enough. We can take a step but it doesn’t mean we are not eventually stuck.
• attempt 3: If $t : T$, then there exists a value $v$ such that $t\rightarrow^* v$.
  • what if program contains infinite loop. That means that we need to solve the halting problem in runtime.
• attempt 4
  • $t$ is eventually stuck if $t \rightarrow^* t'$ and $t'$ is stuck.
  • $t$ is stuck means there does not exist $t'$ s.t. $t \rightarrow t'$.
  • $t$ is not eventually stuck if for all $t'$ s.t. $t \rightarrow^* t'$, $t'$ is not stuck:
    • Either $t'$ is a value or exists $t''$ that $t'\rightarrow t''$.

Theorem (type soundness): if $t: T$ and $t \rightarrow^* t'$, either $t'$ is a value or there exists $t''$ s.t. $t' \rightarrow t''$.

• we allow infinite execution in this form.
• big-step semantics does not allow us infinite execution.

How do we prove this?

Progress + Preservation

Progress and Preservation implies Type Soundness.

Lemma (Progress): “well typed terms are not stuck”.

• If $t : T$, then either $t$ is a value or exists $t'$ s.t. $t \rightarrow t'$.

Lemma (Type Preservation): “stepping preserves well-typedness”

• If $t: T$ and $t \rightarrow t'$, then $t' : T$.

This is actually stronger than the original version. It implies that

• the expression that we step to is well-typed
• the expression that we step to has the same type as before

while the original does not. Let’s prove them!

Lemma (Progress): If $d: (t : T)$, then either $t$ is a value or exists $t'$ s.t. $t \rightarrow t'$.

Proof: by structural induction on t.

• IH: If $t_0 : T_0$ and $t_0$ is a subterm of $t$, then either $t_0$ is a value or exists $t_0'$ s.t. $t_0 \rightarrow t_0'$.
• Case analysis on the root rule in the derivation $d$:
  • Case $T_{Int}$: Then $t=n$ and $T=Int$. So $t$ is a value.
  • Case $T_{Plus}$: Then $t=t1+t2$, $t1: Int$ and $t2: Int$.
    • By IH, either $t1$ is a value or exists $t1'$ s.t. $t1\rightarrow t1'$.
    • By IH, either $t2$ is a value or exists $t2'$ s.t. $t2\rightarrow t2'$.
    • Case analysis on the possibilities of $t1$ and $t2$
      • Case $t1$ is a value and $t2$ is a value:

      • we need a lemma here that says a value of type Int is a number.

        • Since $t1: Int$ and $t2: Int$, by Canonical Forms for Int, $t1 = n1$ and $t2 = n2$. Therefore by $E_{PlusRed}$, $t1 + t2 \rightarrow n$, where $n = n1 [[+]] n2$.
      • Case $t1 \rightarrow t1'$ and $t2 \rightarrow t2'$:
        • Then $t1 + t2 \rightarrow t1' + t2$ by $E_{Plus1}$
      • Case $t1 \rightarrow t1'$ and $t2$ is a value:
        • Then $t1 + t2 \rightarrow t1' + t2$ by $E_{Plus1}$
      • Case $t1$ is a value and $t2 \rightarrow t2'$:
        • Then $t1 + t2 \rightarrow t1 + t2'$ by $E_{Plus2}$
    • …

Lemma (Canonical Forms for Int): If $v: Int$, then $v$ is a number $n$.

• we can prove this by case analysis on the rules without induction.

Alternatively, we can also do structural induction on $d$.

• IH: If $d_0: (t_0 : T_0)$ and $d_0$ is a subderivation of $d$, then either $t_0$ is a value or exists $t_0'$ s.t. $t_0 \rightarrow t_0'$.

In turing complete language, we cannot use structural induction on subterms. We want to focus on structural induction on derivation.

We are going to redo our Progress proof from last time.

Lemma (Progress): If $d: (t : T)$, then either $t$ is a value or exists $t'$ s.t. $t \rightarrow t'$.

We have 2 canonical forms that we can use:

• Lemma (Canonical Forms, Bool): If $v:Bool$, then $v$ is a boolean value $b$.
• Lemma (Canonical Forms, Int): If $v:Int$, then $v$ is a integer value $n$.

Proof: By induction on derivation $d$.

• IH: If $d_0:(t_0:T_0)$, where $d_0$ is a subderivation of $d$, then either $t_0$ is a value or exists $t_0'$ such that $t_0\rightarrow t_0'$.
• Case analysis on the root rule of $d$:
  • Case $T_{Bool}$: Then $t=b$ and $T=Bool$. Then $t$ is value.
  • Case $T_{If}$: Then $t=\texttt{if t1 then t2 else t3}$ and $t_1:Bool$ and
  $t_2:T$ and $t_3:T$.
  • (i propose to use case analysis on $t_1$ but it goes into infinite regress)
  • By IH, $t_1$ is a value or exists $t_1'$ such that $t_1\rightarrow t_1'$.
  • Case analysis on these cases.
    • Case $t_1$ is a value:
      • By Canonical Forms, Bool, either $t_1=true$ or $t_1=false$
      • If former, $t$ steps by $E_{IfTrue}$ otherwise by $E_{IfFalse}$
    • Case $t_1\rightarrow t_1'$:
      • By $E_{If}$, $t$ steps to $\texttt{if t1' then t2 else t3}$
  • Case $T_{Int}$: Then $t=n$ and $T=Int$. Then $t$ is a value.
  • Case $T_{Plus}$: Then $t_1:Int$ and $t_2:Int$.
    • By IH, $t_1$ is either a value or $t_1\rightarrow t_1'$ (we can apply IH since $t_1:Bool$ is a subderivation of $t:Bool$).
    • By IH, $t_2$ is either a value or $t_2\rightarrow t_2'$.
    • Case analysis on these cases:
      • Case $t_1$ is a value and $t_2$ is a value.
        • By Canonical form, Int, $t_1$ is an integer value $n_1$ and $t_2$ is an integer value $n_2$. By $E_{PlusRed}$, $t$ steps.
      • Case $t_1$ is a value and $t_2\rightarrow t_2'$.
        • By $E_{Plus2}$, $t$ steps.
      • Case $t_1\rightarrow t_1'$ and $t_2$ is a value.
        • By $E_{Plus1}$, $t$ steps.
      • Case $t_1\rightarrow t_1'$ and $t_2\rightarrow t_2'$.
        • By $E_{Plus1}$, $t$ steps.
  • (Other cases left as an exercise to the reader)

Note: a type system that rejects all program also satisfies type soundness, since $t:T$ is never true, so the statement is true.

Now we focus on Preservation.

Lemma (Type Preservation): If $d: (t: T)$ and $t \rightarrow t'$, then $t' : T$.

Proof: By induction on derivation $d$.

• IH: If $d_0: (t_0: T_0)$, where $d_0$ is a subderivation of $d$, and $t_0 \rightarrow t_0'$, then $t_0' : T_0$.
• Case $T_{Bool}$: Then $t=b$. Since $t$ is a value, it cannot step.
• Case $T_{If}$: Then $t=\texttt{if t1 then t2 else t3}$, $t_1:Bool$, $t_2:T$, $t_3:T$.
  • case analysis on derivation $t\rightarrow t'$:
    • Case $E_{If}$: $t \rightarrow \texttt{if t1' then t2 else t3}$.
      • By IH, $t1': Bool$
      • By $T_{If}$, $t':T$
    • Case $E_{True}$: $t\rightarrow t_2$: $t_2:T$
    • Case $E_{False}$: $t\rightarrow t_3$: $t_3:T$