Polarized proof-nets and λμ-calculus

We first define Polarized proof-nets, an extension of MELL proof-nets for the polarized fragment of linear logic; the main difference with usual proof-nets is that we allow structural rules on any negative formula. The essential properties (confluence, strong normalization in the typed case) of polarized proof-nets are proved using a reduction preserving translation into usual proof-nets. We then give a reduction preserving encoding of Parigot's lambdamu-terms for classical logic as polarized proof-nets. It is based on the intuitionistic translation: A --> B curved right arrow! A -o B, so that it is a straightforward extension of the usual translation of lambda-calculus into proof-nets. We give a reverse encoding which sequentializes any polarized proof-net as a lambdamu-term. In the last part of the paper, we extend the sigma-equivalence for lambda-calculus to lambdamu-calculus. Interestingly, this new sigma-equivalence relation identifies normal lambdamu-terms. We eventually show that two terms are equivalent iff they are translated as the same polarized proof-net; thus the set of polarized proof-nets represents the quotient of lambdamu-calculus by sigma-equivalence. (C) 2002 Elsevier Science B.V. All rights reserved.