Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 28 novembre, 10h30 ------------- Julien Cretin ------------- INRIA ==================================== On the Power of Coercion Abstraction ==================================== Erasable coercions may be found in languages such as F-eta, F-sub or MLF. They may change the type of terms without changing their behavior and can thus be erased before reduction. 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 describe a restriction of this language with erasable coercions and which subsumes F-eta, F-sub, and MLF.