Background

The problem that we are addressing goes back to at least 1958 with the proposal of a universal computer oriented language (UNCOL). The intervening years have seen many proposals which partially fulfill the original ambitions, the most pertinent to this proposal being the use of the polymorphic lambda calculus in some functional language compilers. Recently a number of people have begun to talk about UML as the new UNCOL but, since we are concerned with assured software, it is important for us that an intermediate language should be supported by a rich theory to allow analysis and reasoning. We have enjoyed some success in using typed $\pi$-calculus in this role [5,,,,,,,,,,68]. Our long-term objective is to consolidate these works and to establish typed $\pi$-calculus and a probabilistic variant as a powerful and widely applicable intermediate language. There are a number of auxiliary objectives that will help us to attain this goal; we need a program analysis framework so that we can automatically verify (certify) and optimise code at this level; we need a way of relating information at the intermediate level to programs at the source level; and we need develop libraries of translation schemes. The main focus of the current proposal is on the first of these: program analysis.