Martin Berger, Kohei Honda and Nobuko Yoshida
 

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.