Strong Normalization of MLF via a Calculus of Coercions

MLF is a type system extending ML with first-class polymorphism as in system F. The main goal of the present paper is to show that MLF enjoys strong normalization, i.e. it has no infinite reduction paths. The proof of this result is achieved in several steps. We first focus on xMLF, the Church-style version of MLF, and show that it can be translated into a calculus of coercions: terms are mapped into terms and instantiations into coercions. This coercion calculus can be seen as a decorated version of system F, so that the simulation results entails strong normalization of xMLF through the same property of system F. We then transfer the result to all other versions of MLF using the fact that they can be compiled into xMLF and showing there is a bisimulation between the two. We conclude by discussing what results and issues are encountered when using the candidates of reducibility approach to the same problem