@article{Remy-Yakobowski@tcs2011:xmlf,
author     = {R{\'e}my, Didier and Yakobowski, Boris},
title      = {A Church-Style Intermediate Language for {MLF}},
journal    = {Theoretical Computer Science},
year       = {2011},
OPTvolume  = {},
OPTnumber  = {},
OPTpages   = {},
OPTmonth   = {},
note = {To appear},
category   = journal,
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. We
exhibit a type preserving encoding of MLF into xMLF, which shows that
xMLF can be used as the internal language for MLF after type inference,
and also ensures type soundness for the most expressive variant of MLF.},
}