Written Assignment (extract from TAPL)
English only

Pure simply typed lambda-calculus (from Fig 9-1 TAPL)
Typing Evaluation
 `x: T ∈ Γ` `Γ |- x: T`
(T-Var)
 `t1 → t'1` `t1 t2 → t'1 t2 `
(E-App1)
 `Γ, x: T1 |- t2: T2` `Γ |- \x: T1. t2: T1 → T2`
(T-Abs)
 `t2 → t'2` `v1 t2 → v1 t'2 `
(E-App2)
 `Γ |- t1: T1 → T2`   `Γ |- t2: T1` `Γ |- t1 t2: T2`
(T-App)
 `(\x:T1.t2). v1` `[x / v1] t2 `
(E-AppAbs)

Lemma 9.3.1 Inversion of the typing relation (without booleans, if)

1. If Γ |- x: R, then x:R ∈ Γ
2. If Γ |- \x: T. t: R, then R=T→S for some S with Γ ⊢ t: S
3. If Γ |- u t: R, then there is some type T such that Γ ⊢ u:T→R and Γ ⊢ t: T

Theorem 9.3.3 Uniqueness of types

In a given typing context Γ, a term t (with all fee variables in the domain of Γ has at most one type. Moreover there is just one derivation of this typing built from the inference rules that generate the typing relation

Simply typed lambda-calculus with subtyping (from Fig 15-1 TAPL)
Typing Subtyping
 `x: T ∈ Γ` `Γ |- x: T`
(T-Var)
 `S <: S`
(S-Refl)
 `Γ, x: T1 |- t2: T2` `Γ |- \x: T1. t2: T1 → T2`
(T-Abs)
 `S <: U`   `U <: T` `S <: T`
(S-Trans)
 `Γ |- t1: T1 → T2`   `Γ |- t2: T1` `Γ |- t1 t2: T2`
(T-App)
 `Γ |- t: S`   `S <: T` `Γ |- t: T`
(T-Sub)
 `T1 <: S1`   `S2 <: T2` `S1 → S2 <: T1 → T2`
(S-Arrow)