A <: B
∆, x : A ⊲ x : B
(ax 1)
!Ac <: B
∆ ⊲ c : B
(ax 2)
∆ ⊲ M : !
n
A
∆ ⊲ inj
l
(M) : !
n
(A ⊕ B)
(⊕.I1)
∆ ⊲ N : !
n
B
∆ ⊲ inj
r
(N) : !
n
(A ⊕ B)
(⊕.I2)
!∆, Γ1 ⊲ P : !
n
(A ⊕ B)
!∆, Γ2, x : !
n
A ⊲ M : C
!∆, Γ2, y : !
n
B ⊲ N : C
Γ1, Γ2, !∆ ⊲ match P with (x 7→ M | y 7→ N) : C
(⊕.E)
Γ1, !∆ ⊲ M : A⊸ B Γ2, !∆ ⊲ N : A
Γ1, Γ2, !∆ ⊲ MN : B
(app)
x : A,∆ ⊲ M : B
∆ ⊲ λx.M : A⊸ B
(λ1)
If F V (M) ∩ |Γ| = ∅:
Γ, !∆, x : A ⊲ M : B
Γ, !∆ ⊲ λx.M : !
n+1
(A ⊸ B)
(λ2)
!∆, Γ1 ⊲ M1 : !
n
A1 !∆, Γ2 ⊲ M2 : !
n
A2
!∆, Γ1, Γ2 ⊲ hM1, M2i : !
n
(A1 ⊗ A2)
(⊗.I)
∆ ⊲ ∗ : !
n
⊤
(⊤)
!∆, Γ1 ⊲ M : !
n
(A1 ⊗ A2) !∆, Γ2, x1:!
n
A1, x2:!
n
A2 ⊲ N : A
!∆, Γ1, Γ2 ⊲ let hx1, x2i = M in N : A
(⊗.E)
!∆, f : !(A ⊸ B), x : A ⊲ M : B !∆, Γ, f : !(A⊸ B) ⊲ N : C
!∆, Γ ⊲ let rec f x = M in N : C
