Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract)
Roberto Di Cosmo, Delia Kesner · 1997
) Roberto Di Cosmo DMI-LIENS (CNRS URA 1347) Ecole Normale Superieure 45, Rue d'Ulm 75230 Paris Cedex, France Email:[email protected] Delia Kesner LRI (CNRS URA 410) Bat 490 Universite de Paris-Sud 91405 Orsay Cedex, France Email:[email protected] Abstract In this paper, 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 #x-calculus [34, 5] is strongly normalizing, as well as of all the calculi that can be translated to it keeping normalization properties such as # # [27], # s [22], # d [24], and # f [14]. 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 identifications of proofs in Linear Logic that differ by inessential details. These...