Typed symmetric lambda-calculus is the simplest computational
interpretation of classical logic with an involutive negation. Its
main distinguishing feature is to be a true non-confluent
computational interpretation of classical logic which intends to
reflect the computational freedoom given by classical logic,
compared to intuitionnistic logic.
Barbanera and Berardi proved in [1,2] that first order
typed symmetric lambda-calculus enjoys strong normalisation property
and showed in [3] that it can be used to derive symmetric
programs, which could not be derived in a the usual confluent
systems.
In this paper we prove that second order typed symmetric
lambda-calculus enjoys strong normalisation property. As far as we
know, this is the first strong normalisation proof for a second
order essentially non-confluent system.
