To: seminaire@pauillac.inria.fr From: Didier.Remy@inria.fr Subject: SEM - INRIA : Cristal - 20/06/03 - Paris - FR Vous pouvez maintenant vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E . ___ / _ _ / _ / / / \ / \ / / __| / |___ |_/ |_/ / |__ |_/ |_ ___ . / / ___ __ /_ _ / _/ /| /| _ __ __ _ _ / / / /_ / __| / / |/ | / \ /_ / / \ | / __| |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ I N R I A - Rocquencourt Salle de conférence du Bat 8 Vendredi 20 juin, 10h30 ------------------------------------ Virgile Prevosto et Stephane Fechter ------------------------------------ Universite de Paris 6 (LIP6) ======================================= Matinee FOC: semantique et compilation. ======================================= 10h30 - 11h30 (Stephane Fechter) Fondements sémantiques de FoC FOC a d'abord été conçu pour passer progressivement de la spécification à l'implantation de structures mathématiques. Le langage obtenu propose un certain nombre de traits objets et également une notion d'encapsulation. Nous présentons un système de type et une sémantique opérationnelle basée sur un modèle orientée objet pour ce langage. 11h30 - 12h30 (Virgile Prevosto) Objets ou Enregistrements ? La compilation d'une hiérarchie de structures algébriques en Ocaml et Coq FoC est un langage dédié au calcul formel certifié implanté au dessus de Ocaml et Coq. Comme le présente Stéphane Fechter dans l'exposé précédent, la hiérachie de structures mathématiques offerte par FoC peut se décrire à l'aide d'une sémantique orientée-objet. Grosso modo, une structure algébrique correspond à une classe et une opération correspond à une méthode. Par ailleurs, l'absence de mécanismes objets en Coq a conduit à proposer une traduction basée sur des enregistrements et des "générateurs de méthodes". Ces derniers sont des lambda-abstractions permettant de retrouver un des aspects essentiels (pour FoC) de la programmation objet, la liaison retardée. Dans cet exposé, on montrera tout d'abord comment est réalisée concrètement la traduction d'une structure FoC en une classe Ocaml et en Coq. Nous verrons également qu'une traduction basée sur des enregistrements est également possible en Ocaml, et comparerons l'efficacité de ces deux approches à partir d'exemples tirés de la librairie actuelle de FoC.