Programme

Mardi 21 mai

Thème abordé : Logique et théorie de types

Intervenants : Bruno Barras et Benjamin Werner (INRIA) - Bruno.Barras@inria.fr, Benjamin.Werner@inria.fr

Mots-clés : Logiques, preuves constructives, types, Coq.

Référence :

- A Tutoral on Recursive Types in Coq, Edouardo Giménez

- The Coq Proof Assistant-A Tutorial-Version 6.3.1, Gérard Huet, Gilles Kahn and Christine Paulin-Mohring

 

Mercredi 22 mai

Thème abordé : Programmation synchrone pour les systèmes réactifs

Intervenants : Nicolas Halbwachs (Verimag/CNRS) et Florence Maraninchi (Vermag/INPG) - Nicolas.Halbwachs@imag.fr, Florence.Maraninchi@imag.fr

Mots-clés : Langages synchrones, Lustre, Esterel, Automates de mode, Compilation, Vérification.

Référence : N. Halbwachs, Synchronous programming of reactive systems - Kluwer Academic Pub., 1993

Jeudi 23 mai

Thème abordé : Introduction à la méthode formelle B

Intervenant : Mireille Ducassé (IRISA/INSA) - Mireille.Ducasse@irisa.fr

Mots-clés : formalisation, preuve, spécification, raffinement, implémentation, études de cas

Références :

- Jean-Raymond, The B Book. Assigning Programs to Meanings - Cambridge University Press, 1996.

- Mireille Ducassé and Laurence Rozé, Proof obligations of the B formal method : local proofs ensure global consistency, In LOgic-based program Synthesis and TRansformation, 1999 - Springer-Verlag, Lecture Notes in Computer Science 1817.

Vendredi 24 mai

Thème abordé : Programmation par contraintes

Intervenants : François Fages (INRIA) et Andreas Podelski - Francois.Fages@inria.fr, podelski@mpi-sb.mpg.de

Mots-clés : Logique et programmation: le paradigme de la programmation logique

- Programmes = Théories, Exécution = Recherche de preuves,

- La classe des langages de programmation logique avec contraintes CLP (X),
- Exemples CLP (H), CLP (lambda), CLP (R), CLP (FD), et démonstrations,
- Propriétés observables et équivalences des programmes,
- Complète adéquation des sémantiques opérationnelles et de point fixe,
- Théorèmes de complétudes pour la sémantique logique.

une vue CLP du model checking et de l'analyse de programme

- Systèmes concurrents à nombre d'états infinis,
- Logique CTL et preuve de programmes,
- Traduction des systèmes concurrents en des programmes logiques,
- Model checking symbolique et interprétation abstraite.

Lundi 27 mai

Thème abordé : Typage et calcul pour la mobilité et la sécurité

Intervenant : Michele Bugliesi (Université Ca' Foscari, Venise, département informatique) - michele@dsi.unive.it

Synopsis :

• foundations for concurrency and mobility

  - from the pi-calculus to calculi of mobile agents

  - Ambients, Seals, D-pi calculus

• type systems

  - for the pi-calculus

  - for mobile agents

• security by typing

  - resource access and information flow

  - secrecy and authentification

Références : All topics covered in the course are based on research papers. Relevant references will be provided with the course material.

Mardi 28 mai

Thème abordé : De la technologie des objets à la technologie des modèles

Intervenant : Jean Bézivin (Université de Nantes) - Jean.Bezivin@sciences.univ-nantes.fr

Mercredi 29 mai

Thème abordé : Formalization, design and implementation of Object Oriented Languages

Intervenant : Sophia Drossoupoulou (Imperial College, GB) - sd@doc.ic.ac.uk

Mots-clés : formalization, object oriented, types, implementation, byte-code verification, binary compatibility, linking, loading

Synopsis :

1. a minimal formal, object oriented, class based, imperative language
2. formalizing and implementing overloading
3. multimethods and separate compilation
4. formalizing byte-code verification
5. dynamic linking, multiple loaders and verification, binary compatibility
6. object based calculi, ingeritance via delegation

Références :

- Is the Java Type System Sound ?, Sophia Drossopoulou, Susan Eisenbach and Sarfraz Khurshid - Theory and practic of Object Systems, Volume 5 (1), p. 3-24, 1999, also at http://www-dse.doc.ic.ac.uk/projects.slurp.pubs.html
- What is Java binary compatibility ?, Sophia Drossopoulou, David Wragg, Susan Eisenbach - OOPSLA'98, also from http://www-dse.doc.ic.ac.uk/projects/slurp/pubs.html
- Towards an abstract model of Java dynamic linking and verification, Sophia Drossopoulou - TIC'2000, and from http://www-dse.doc.ic.ac.uk/projects/slurp/pubs.html
- A theory of objects, Martin Abadi, Cardelli - Springer Verlag, more at http://www.luca.demon.co.uk/TheoryOfObjects.html
- A type system for Java bytecode subroutines, Raymie Stata, Martin Abadi - POPL 198 : 149-160, more at http://gatekeeper.dec.com/pub/DEC/SRC/research-reports/abstracts/src-rr-158.html

 

Jeudi 30 mai

Thème abordé : Objets, concurrence, répartition et mobilité

Intervenant : Denis Caromel (INRIA) - Caromel@sophia.inria.fr

Synopsis :

- Objets standards vs. Activité vs.Objets actifs,
- Dimensions fondamentales,
- Héritage et polymorphisme pour la répartition,
- Communications et Synchronisations inter-objets,
- Programmation des activités et des synchronisations intra-objet,
- Réactivité et mobilité
- Un peu de réflexion, des exemples et des outils interactifs

Références :

- Object-oriented parallel and distrubuted programming, J-P. Bashoun, T. Baba, J-P. Briot, A.Yonezawa - HERMES Science Publicatoins, ISBN N°2-7462-0091-0, 1999.
- Parallel programming using C++, G. Wilson and P. Lu - MIT Press1996 ISBN N°0-262-73118-5.
- Concurrent object-oriented programming, CACM, Communications of the ACM, Volume 36, Number 9, September 1993.

Vendredi 31 mai

Thème abordé : Test de logiciels

Intervenants : Thierry Jéron et Yves Le Traon (INRIA), Thierry.Jeron@irisa.fr, Yves.Le_Traon@irisa.fr

Haut de page