A denotational semantics ofLC2

The aim of this paper is to extend the classical sequent calculusLC to the second order. This task is realized by a semantical approach mixing the correlation spaces semantics ofLC on the one hand, and the analogy with the interpretation of systemF in coherent spaces on the other hand. This relies on the introduction of a new semantical object:noetherian correlation spaces.From the semantics we deduce the syntax of the second order classical sequent calculusLC2.