The Applied pi-calculus: Type Systems and Expresiveness

Bloch, Anders ; Frederiksen, Morten V. ; Haagensen, Bjørn

4. term

Computer Science, Master

2004

2012-02-14

In this master thesis we present an encoding of the Applied pi-calculus (AppPi) in the pi-calculus and it is shown how AppPi can be instantiated to obtain the spi-calculus. Furthermore, we define two type systems for AppPi. One is a basic type system capable of capturing errors such as arity mismatch and erroneous use of names. The other is a type system equivalent to the type system for the spi-calculus for checking security properties proposed by Abadi. It is shown that the representation of the spi-calculus preserves types with respect to this type system. The encoding of the spi-calculus in the instance of AppPi is shown to be sound and complete with espect to operational correspondence. In order to facilitate the proof of this result a semantics for the spi-calculus in the same style as the semantics for AppPi is used, i.e. an early labelled transition relation. This modified semantics is shown to be strongly equivalent to that of the originally proposed by Abadi and Gordon which uses the notion of abstractions and concretions. We do not directly encode the equational theory used in AppPi, rather we rely on well-known results for transforming such a theory into a confluent and terminating rewrite system on which the encoding is performed. The encoding is shown to be sound with respect to operational correspondence. In light of the sparse amount of work which has followed the original publication of AppPi, one of the major assets of our encoding is that it makes the vast amount of theoretical and practical tools developed for the pi-calculus available for reasoning in AppPi.

Download
View record in AAU Student Projects