Genericity and the Pi-Calculus
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 including a full abstraction of an encoding of System F, the second-order polymorphic lambda-calculus.
Download: ps.gz, pdf (extended abstract), ps.gz, pdf (full version). Bibtex.
$Id: index.html,v 1.1 2004/09/23 09:22:41 martinb Exp martinb $