Pure simply typed lambdacalculus (from Fig 91 TAPL)

Typing

Evaluation


t_{1} → t'_{1}  t_{1} t_{2} → t'_{1} t_{2} 
 (EApp1) 

Γ, x: T_{1}  t_{2}: T_{2}  Γ  \x: T_{1}. t_{2}: T_{1} → T_{2} 
 (TAbs) 

t_{2} → t'_{2}  v_{1} t_{2} → v_{1} t'_{2} 
 (EApp2) 

Γ  t_{1}: T_{1} → T_{2} Γ  t_{2}: T_{1}  Γ  t_{1} t_{2}: T_{2} 
 (TApp) 

(\x:T_{1}.t_{2}). v_{1}  [x / v_{1}] t_{2} 
 (EAppAbs) 

Lemma 9.3.1 Inversion of the typing relation (without booleans, if)
 If Γ  x: R, then x:R ∈ Γ
 If Γ  \x: T. t: R, then R=T→S for some S with
Γ ⊢ t: S
 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 lambdacalculus with subtyping (from Fig 151 TAPL)

Typing

Subtyping



Γ, x: T_{1}  t_{2}: T_{2}  Γ  \x: T_{1}. t_{2}: T_{1} → T_{2} 
 (TAbs) 


Γ  t_{1}: T_{1} → T_{2} Γ  t_{2}: T_{1}  Γ  t_{1} t_{2}: T_{2} 
 (TApp) 

Γ  t: S S <: T  Γ  t: T 
 (TSub) 

T_{1} <: S_{1} S_{2} <: T_{2}  S_{1} → S_{2} <: T_{1} → T_{2} 
 (SArrow) 

