In this papel; we show the correspondence existing between normalization in calculi with explicit substitution and cut elimination in sequent calculus for Linear Logic, via Proof Nets. This correspondence allows us to prove that a typed version of the Xx-ccilculus [34, 51 is strongly normalizing, as well as of all the calculi that can be translated to it keeping normalization properties such as A, [271, A, 1.221, Ad 1241, arid Xf 1141. In order to achieve this result, we introduce a new notion of reduction in Proof Nets: this extended reduction is still confluent and strongly normalizing, and is of interest of its own, as it corresponds to more identiJicatioris of proofs in Linear Logic that differ by inessential details. These results show that calculi with explicit substitutions are reully an intermediate formalism between lambda calculus and proof nets, und suggest a completely new way to kook at the problems still open in thejeld of explicit substitutions.
['Roberto Di Cosmo', 'Delia Kesner']
Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract)