Untyped lambda calculus
terms and values
x I M M I Ax.M V ::= Ax.M
full (3-reduction evaluation rules
terms value
Mi M2
(Ax.M) N ^ß M[x := N]
Mi M2 Mi N —^ß M2 N
Ax.Mi Ax.M2
Ni ^ß N2 M Ni —^ß M N2
call-by-value evaluation rules
Mi ^cbv M2
Ni
cbv
N2
(Ax.M) V ^cbv M[x := V] Church numerals and booleans
Af.Ax.x Af .Ax.f x
MiN^cbvM2N VNi^cbvVN2
true := Ax.Atj.x false := Ax.Atj.tj
n := Af.Ax. f (f... (f (x)...) = Af.Ax.fn(x)
n-times
Simply-typed lambda calculus A
with Booleans
terms and values
M ::= x | M M | Ax: ct.M | true | false | if M then M else M terms
V ::= Ax: ct.M I true I false values
types
typing rules
ct ::= ct —> ct | Bool
r h true : Bool (T-True) r h false : Bool (T-False) x: ct £ r
F h x: ct r,x:ct h M:t
T h Ax: ct.M : ct —y x
F h M: ct —>• t     r h N : ct Th MN:t
r h M: Bool     F h N : er     F h L: cr
T h if M then N else L: ct
(T-Var)
(T-Abs) (T-App)
(T-If)
Hindley-Milner type system
terms and values
types
typing rules
M ::= x I M M I Ax.M I let x = M in M
t ::= a \ x —> x monotypes a ::= t I Vcc.cr type schemes
x : er e r (x_var)
T h x : ct T,x:Th M:t'
T h Ax.M.: t —y x
f hlVl: t -> t'     F h N : t r h M N : t'
f h M : ct     r,x: eh N :t T I- let x = M in N : t
T h M : ct'     ct' C ct
— (T-Abs)
(T-App) (T-Let)
r h M : ct
(t-lNST)
r h M.: ct     oitFVir) (T_GEN) r h M : Voc.cr
System F
terms and values
M ::= x I M M | Ax : ct.M | Aa.M | M [a] terms V ::= Ax : ct.M. I Aa.M values
types
ct ::= a I er —> er I V(x.ct
typing rules (in addition to A-5-)
rhM:g_«gmn (t.tabs) (t-gen)
rhAa.M:Va.cr
r h M: Va.CT      (T.TApp) (T-Inst)
T h M [ct'] : {ct'/cx}ct evaluation rules (in addition to A^J
M     M' (E.TAPP)
M [ct] -> M' [ct] (Aa.M) [ct] -> {cr/a}M (E-TAppTAbs)