To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 18/05/09 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.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 18 mai, 10h30 ----------------- Nicolas Pouillard ----------------- INRIA ======================== Towards a Not-so-FreshML ======================== The semantics of FreshML dictates that inspecting an abstraction (by pattern matching against it) causes its bound atom to be renamed into a fresh atom. This guarantees that all atoms "live in the same world": they can be meaningfully compared, without risk of two atoms being "accidentally equal". This approach, however, is sometimes inefficient: there are quite a few practical situations where renaming is unnecessary. We argue that inspecting an abstraction without renaming its bound atom can be safe, provided one keeps track of the fact that inside and outside of the abstraction are different "worlds", and provided one forbids comparisons between atoms that inhabit different worlds. By making worlds explicit, we hope not only to achieve better efficiency, but also to offer a new, more flexible set of primitive concepts for describing the structure of data-with-binding. (This is work in progress.)