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.