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}
![Previous page](../images/prev.gif)
![Contents](../images/toc.gif)
![Next page](../images/next.gif)