ML^F 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 ML^F 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 xML^F, the Church-style version of ML^F, 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 result entails strong normalization of xML^F through the same property of system F. We then transfer the result to all other versions of ML^F using the fact that they can be compiled into xML^F 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.
['Giulio Manzonetto', 'Paolo Tranquilli']
Strong normalization of MLF via a calculus of coercions