%% inria-00582570, version 2
%% http://hal.inria.fr/inria-00582570/en/
@techreport{Cretin-Remy:coercions@inria2001,
HAL_ID = {inria-00582570},
URL = {http://hal.inria.fr/inria-00582570/en/},
title = {{E}xtending {S}ystem {F}-eta with {A}bstraction over
{E}rasable {C}oercions},
author = {Cretin, Julien and R{\'e}my, Didier},
abstract = {{E}rasable coercions in {S}ystem {F}-eta, also known as
retyping functions, are well-typed eta-expansions of the identity. {T}hey
may change the type of terms without changing their behavior and can thus
be erased before reduction. Coercions in {F}-eta can model subtyping of
known types and some displacement of quantifiers, but not subtyping
assumptions nor certain form of delayed type instantiation. We generalize
F-eta by allowing abstraction over retyping functions. We follow a general
approach where computing with coercions can be seen as computing in the
lambda-calculus but keeping track of which parts of terms are
coercions. We obtain a language where coercions do not contribute to the
reduction but may block it and are thus not erasable. We recover erasable
coercions by choosing a weak reduction strategy and restricting coercion
abstraction to value-forms or by restricting abstraction to coercions that
are polymorphic in their domain or codomain. The latter variant subsumes
{F}-eta, {F}-sub, and {MLF} in a unified framework.},
language = {{E}nglish},
affiliation= {{GALLIUM} - {INRIA} {R}ocquencourt - {INRIA} },
pages = {64},
type = {{R}esearch {R}eport},
institution= {INRIA},
number = {{RR}-7587},
month = Jul,
year = {2011},
PDF = {http://hal.inria.fr/inria-00582570/PDF/full.pdf},
}