As usual, the typing judgment \(\Delta ; \Gamma |- e : S\) 
denotes that “the expression e has type \(S\)  under the type variable environment \(\Delta \)  and the type environment \(\Gamma \) ”.
The typing rules are mostly standard [1]}.
Here, we only discuss the special treatment of security types.
<FIGURE>