Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi

We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of λ-calculus by means of intersection type systems. The method is first illustrated by applying to a composition-free calculus of explicit substitutions, yielding a simpler proof than the previous one by Lengrand et al. Then we present a new intersection type system in the style of sequent calculus, and show that it characterizes the strongly normalizing terms of Dyckhoff and Urban’s extension of Herbelin’s explicit substitution calculus.

• Type: Conference
• Year: 2007
• Where: RTA
• Authors: Kentaro Kikuchi
• Keywords: Explicit Substitution, Intersection Type, RTA 2007, Strongly Normalizing, Theoretical Computer Science