Strong normalization of via a calculus of coercions

Abstract: is a type system extending with first-class polymorphism as in system . The main goal of the present paper is to show that 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 , the Church-style version of , 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 , so that the simulation result entails strong normalization of through the same property of system . We then transfer the result to all other versions of using the fact that they can be compiled into 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. [Copyright &y& Elsevier]