SE547: Subtyping [11/23]

Subtyping:

• τ <: τ' means τ' is a higher security class than τ (e.g. L <: H)
• τ var <: τ' var if τ <: τ' (covariant)
• τ' cmd <: τ cmd if τ <: τ' (contravariant)
• Subtyping is reflexive (and transitive). All types are subtypes of themselves (τ <: τ)

Allows for more complex set of security classes (e.g. {H,L1,L2 | L1 <: H & L2 <: H}