To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 25/06/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 Salle de réunion du bâtiment 11 Jeudi 25 juin, 10h30 -------------------- Alexandre Pilkiewicz -------------------- INRIA ========================================================== Destins et prédictions: une autre approche de la monotonie ========================================================== La littérature propose, grossièrement, deux possibilités pour typer les références mutables: 1) La plus répandue, celle de ML, Java et tous les autres, autorise un aliasing sans restriction mais impose que le type de la référence soit défini une fois pour toutes à la création. 2) La seconde possibilité consiste à conserver un contrôle strict de l'aliasing mais donne en échange à l'unique possesseur de la référence tous les droits sur celle-ci: il peut y lire et écrire, mais aussi changer son type, voire la désallouer. La contrepartie est l'utilisation d'un système de types linéaires. Même si les approches avec capacités et régions apportent une certaine souplesse, la restriction reste de taille. Le but de cet exposé est de présenter une solution intermédiaire: en imposant aux écritures de se faire de façon *monotone*, on relâche la contrainte d'aliasing de la seconde possibilité tout en autorisant une forme réduite de strong-update. L'approche que nous proposons, à base de destins et de prédictions, est bien plus générale qu'une notion ad-hoc de références monotones. Nous la présenterons à travers trois exemples: - les compteurs entiers monotones nous permettront d'introduire notions et notations; - nous montrerons ensuite comment les destins permettent de typer des thunks "à la Danielsson" pour évaluer des propriétés de complexité amortie d'un programme; - nous finirons par une application au typage du hash-consing.