A Church-Style Intermediate Language for MLF

MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during reduction. All paramefunctions are explicitly typed and both type abstraction and type instantiation are explicit. However, type instantiation in xMLF is more general than type application in System F. We equip xMLF with a smallstep reduction semantics that allows reduction in any context and show that this relation is confluent and type preserving. We also show that both subject reduction and progress hold for weak-reduction strategies, including call-by-value with the value-restriction. We exhibit a type preserving encoding of MLF into xMLF, which ensures type soundness for the most general version of MLF. We observe that xMLF is a calculus of retyping functions at the type level.

• Type: Conference
• Year: 2010
• Where: FLOPS
• Authors: Didier Rémy, Boris Yakobowski
• Keywords: FLOPS 2010, Hardware, System F, Type Instantiation, Type System