The -calculus is a process calculus in which we can compositionally represent dynamics of major
programming constructs by decomposing them into a single communication primitive, the name
passing. This work reports our experience in using a linear/aÆne typed -calculus for the analysis
and development of type-based analyses for programming languages, focussing on secure information

ow analysis. After presenting a basic typed calculus for secrecy, we demonstrate its usage
by a sound embedding of the dependency core calculus (DCC) and the development of the callby-
value version of DCC. The secrecy analysis is then extended to stateful computation, using
which we develop a novel type discipline for imperative programming language which extends
a secure multi-threaded imperative language by Smith and Volpano with general references and
higher-order procedures. In each analysis, the embedding gives a simple proof of noninterference.