Harnessing MLF with the Power of System F

We provide a strong normalization result for MLF , a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating MLF into a calculus of coercions, and showing that this calculus is just a decorated version of system F.

• Type: Journal
• Year: 2010
• Where: MFCS
• Authors: Giulio Manzonetto, Paolo Tranquilli
• Keywords: Calculus, Generalizing, MFCS 2010, Theoretical Computer Science, first-class Polymorphism