Newsgroups: fr.announce.seminaires Distribution: fr To: fr-sem@frmug.org From: Didier.Remy@inria.COUPER-CECI.fr Organization: INRIA-Rocquencourt Subject: SEM - INRIA : Cristal - 06/10/00 - Paris - FR http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ . / _ _ / ___ __ /_ _ / /| /| _ __ __ _ _ / / \ / \ _ / / / /_ / __| / _ / |/ | / \ /_ / / \ | / __| |___ |_/ |_/ |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ / / I N R I A - Rocquencourt, Salle de conference du Bat 11 ------------------- Vendredi 6 octobre ------------------- =========================================================== 10h15 - 11h15 : What is a file synchronizer? par Benjamin C. Pierce, Université de Pennsylvanie 11h15 - 11h45 : Pause café 11h45 - 12h45 : Functional Nets par Martin Odersky, Ecole Polytechnique de Lausanne 14h30 - 15h30 : Typer XML à l'aide d'expressions rationnelles par Jérome Vouillon, Université de Pennsylvanie =========================================================== ----------------------------- What is a file synchronizer? ----------------------------- Benjamin C. Pierce, Université de Pennsylvanie Mobile computing devices intended for disconnected operation, such as laptops and personal organizers, must employ optimistic replication strategies for user files. Unlike traditional distributed systems, such devices do not attempt to present a ``single filesystem'' semantics: users are aware that their filesystems are replicated, and that updates to one replica will not be seen in another until some point of synchronization is reached (often under the user's explicit control). A variety of tools, collectively called FILE SYNCHRONIZERS, support this mode of operation. Descriptions of present-day synchronizers seldom give the user enough information to predict how they will behave under all circumstances. Simple slogans like ``Non-conflicting updates are propagated to other replicas'' ignore numerous subtleties---e.g., Precisely what constitutes a conflict between updates in different replicas? What does the synchronizer do if updates conflict? What happens when files are renamed? What if the directory structure is reorganized in one replica? The main goal of this talk is to offer a simple, concrete, and precise framework for describing the behavior of file synchronizers. Some design and engineering aspects of our own file synchronizer, called Unison (http://www.cis.upenn.edu/~bcpierce/unison), will also be discussed. ---------------- Functional Nets ---------------- Martin Odersky, Ecole Polytechnique de Lausanne Functional nets arise out of a fusion of the essential ideas of functional programming in Petri Nets. As in functional programming, the basic computation step in a functional net rewrites function applications to function bodies. As in Petri-Nets, a rewrite step can require the combined presence of several inputs (where in this case inputs are function applications). This fusion of ideas from two different areas results in a style of programming which is at the same time very simple and very expressive. This talk introduces functional nets with a series of examples, taken from a broad range of programming areas and styles. We will model key constructs of functional, imperative, and concurrent programming, and will show how objects can be expressed in a flexible way through the use of qualified definitions. Functional nets have a theoretical foundation in Join calculus. The talk will review Join calculus and show how functional nets relate to it. ---------------------------------------------- Typer XML à l'aide d'expressions rationnelles ---------------------------------------------- Jérome Vouillon, Université de Pennsylvanie XDuce est un langage fortement typé destiné à manipuler des document XML. Les types de XDuce sont des expressions rationnelles, généralisation naturelle des DTD. Une relation de sous-typage très puissante peut être définie sur ces types, tout simplement comme la relation d'inclusion des dénotations des types. Vérifier une telle inclusion est EXPTIME-complet en théorie (inclusion d'automates d'arbres). Cependant, les types apparaissant effectivement dans les programmes sont relativement simples, bien que pouvant être très larges. En exploitant ce fait, nous avons conçu un algorithme de vérification de sous-typage se comportant bien en pratique.