Proof Nets and Explicit Substitutions

International audienceWe refine the simulation technique introduced in [Di Cosmo and Kesner, 97] to show strong normalization of lambda-calculi with explicit substitutions via termination of cut elimination in linear logic proof nets [Girard, 87]. We first propose a notion of equivalence relation for proof nets that extends the one in [Di Cosmo and Guerrini, 99], and we show that cut elimination modulo this equivalence relation is terminating. We then show strong normalization of the typed version of the lambda-l-calculus with de Bruijn indices (a calculus with full composition defined in [David and Guillaume, 99]) using a translation from typed lambda-l to proof nets. Finally, we propose a version of typed lambda-l with named variables which helps to better understand the complex mechanism of the explicit weakening notation introduced in the lambda-l-calculus with de Bruijn indices [David and Guillaume, 99]