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.