zbMATH — the first resource for mathematics

Genericity and the \(\pi\)-calculus. (English) Zbl 1029.68039
Gordon, Andrew D. (ed.), Foundations of software science and computations structure. 6th international conference, FOSSACS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2620, 103-119 (2003).
Summary: We introduce a second-order polymorphic \(\pi\)-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical development on polymorphic calculi in the past. This allows precise embedding of generic sequential functions as well as seamless integration with imperative constructs such as state and concurrency. Two behavioural theories are presented and studied, one based on a second-order logical relation and the other based on a polymorphic labelled transition system. The former gives a sound and complete characterisation of the contextual congruence, while the latter offers a tractable reasoning tool for a wide range of generic behaviours. The applicability of these theories is demonstrated through non-trivial reasoning examples and a fully abstract embedding of System F, the second-order polymorphic \(\lambda\)-calculus.
For the entire collection see [Zbl 1017.00036].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
Full Text: Link