Against the background discussed in Section 1, the central aim of the
present project is to investigate the feasibility of using the 
-calculus
as a general foundation of PA technologies. We choose
qualitative/quantitative IFA as a concrete domain in which we experiment our
thesis. Concrete objectives are: (1) the extension of the typed
-calculus to cover all major language constructs, including genericity
and synchronisation: (2) the development of theory of quantitative secrecy in
the context of typed -calculi; and (3) development of prototypical PA
tools based on the developed theories, applied to concrete programs with
security concerns.