@incollection {Remy-Yakobowski@flops2010:xmlf,
AUTHOR = {R{\'e}my, Didier and Yakobowski, Boris},
AFFILIATION = {INRIA Paris - Rocquencourt},
TITLE = {A Church-Style Intermediate Language for MLF},
BOOKTITLE = {Functional and Logic Programming},
SERIES = {Lecture Notes in Computer Science},
EDITOR = {Blume, Matthias and Kobayashi, Naoki and Vidal, German},
PUBLISHER = {Springer Berlin / Heidelberg},
PAGES = {24-39},
VOLUME = {6009},
URL = {http://dx.doi.org/10.1007/978-3-642-12251-4_4},
DOI = {10.1007/978-3-642-12251-4_4},
ABSTRACT = 
  {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 parameters
  of functions 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 small-step
  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.},
YEAR = {2010}
}