Figure REF  presents the syntax of \(\mathsf {\lambda }^{\exists }_{\mathsf {SEC}}\) . Expressions \(e\)  are completely standard [1]}, including functions, applications, variables, primitive values
, binary operations on primitive values, the unit value, pairs with their first and second projections, injections \(\mathsf {inl}~e\)  and \(\mathsf {inr}~e\)  to introduce sum types, as well as a \(\mathsf {case}\) 
construct to eliminate sums; finally, \(\mathsf {pack}\)  and \(\mathsf {open}\)  introduce and eliminate existential packages, respectively.
Types \(T\)  include
function types \(S->S\) , primitive types \(P\) , the unit type \(\mathsf {1}\) , sum types \(S+S\) , pair types
\(S\times S\) , existential types \(\exists X.T\) , type variables \(X\)  and the top type \(\top \) . A security type \(S\) 
is a faceted type \({T}@{U}\)  where \(T\)  is the safety type and \(U\)  is the declassification type.
<FIGURE>