@InProceedings{Cretin-Remy:coercions@popl2012,
title = {{O}n the {P}ower of {C}oercion {A}bstraction},
author = {Cretin, Julien and R{\'e}my, Didier},
booktitle =
{Proceedings of the 39th {ACM} Symposium on Principles
of Programming Languages (POPL 2012)},
year = 2012,
address = {Philadephia, PA, USA},
month = jan,
category = conference,
note = {To appear},
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.},
ALSO = {http://gallium.inria.fr/~remy/coercions/},
}