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 8 mars, 10h30 --------------- Benoît Montagu --------------- INRIA ====================================================== Small-step extensional equivalence for singleton types ====================================================== Singletons are the key ingredient to model type definitions in modern designs for modules à la ML. They provide a very powerful equivalence relation on types. This equivalence is also quite subtle, since it is sensitive to the environment and to the kind at which types are considered, which makes deciding type equivalence a non trivial task. In this talk, we will introduce the singleton type system, its particularities and the difficulties it raises. Then, we will sketch an ongoing work on singletons, where equivalence is defined as the reflexive symmetric transitive closure of a reduction relation that is based on β-reduction and η-expansion, and that is proved confluent and strongly normalizing.