Réunions
De CeProMi.
Sommaire |
Réunion pleniere du 23-24 septembre, Orsay
Planning prevu
- mercredi 23 apres-midi
- groupe de travail 1 (Elena, Alain, Claude): finalisation du travail d'Elena
- jeudi 24 matin
- 9:30 Asma Tafat: Raffinement de Programmes Java
- 10:00 Elena Tushkanova: Modular specifications of Java programs
- 11:00 Severine Maingaud: Preuves de programmes d'ordre supérieur avec traits impératifs
- 11:30 [1] Johannes Kanig: Un outil pour la preuve de programmes d'ordre supérieur (présenté au Workshop ML 2009)
- jeudi 24 apres-midi
- groupe de travail 2 (Asma, Sylvain, Claude): raffinement en presence de partage
Participants
- DCS/Grenoble
- Sylvain Boulmé (seulement le 24)
- Cassis/Besancon
- Alain Giorgetti
- Elena Tushkanova
- Proval/Orsay
- Claude Marché
- Asma Tafat
- Romain Bardou
- Johannes Kanig
- Wendi Urribarrí (seulement le 23)
- Gallium/Rocquencourt
- Arthur Charguéraud
- Francois Pottier
- PPS/Paris
- Yann Regis-Gianas
- Severine Maingaud
Réunion du 20-24 juillet 2009, Grenoble
Participants
- Grenoble.
- Sylvain Boulmé
- Marie-Laure Potet
- Cassis
- Alain Giorgetti
- Elena Tushkanova
- Proval
- Claude Marché
- Christine Paulin-Mohring
- Wendi Urribarrí
- Asma Tafat
Exposés
- Modules and Refinement in Why [2] (W. Urribarrí et C. Paulin)
- Example of Collection & Iterators in Java (using "unpack" and "pack with") by S. Boulmé: see TestIterator.java (a single iterator) and TestIterators.java (several iterators) in svn directory "arc2008/stageAsma/Examples".
Réunion du 12-13 mars 2009, Grenoble
Programme
jeudi 12 mars
- 12h, accueil des participants, centre equation [3]
- 12h30 repas sur place
- 14h exposé 1: Johannes Kanig, « calcul de plus faibles préconditions pour les programmes impératifs d'ordre supérieur » [4]
- 15h exposé 2: Manuel Garnacho, « Presentation d'un protocole de communication pour systeme reactif »
- 16h pause
- 16h20 Francois: regle anti-frame generalisee [5]
- 16h45 Alexandre: monotonie
- 19h30 Diner au Caffe Forte, 4, Place Lavalette [6]
vendredi 13 mars
- 9h Romain: invariants et effets caches via regions et capacités. Slides : [7]
- 9h45 Arthur: champs "model". Slides:[8]
- 10h groupe de travail sur gestion des invariants par régions et capacités
- 10h30 exposé 3: Wendi Urribarrí, « composition de modules en Why » [9]
- 11h15 groupe de travail: ownership et raffinement en Java et en B
- 12h bilan et futur
- 12h30: repas
- apres-midi discussion pour ceux qui ont le temps
Exposés prévus
- Exposé de Johannes sur un calcul de plus faibles préconditions qui traite les programmes impératifs d'ordre supérieur
- Suite des travaux sur typage avec regions/capacités des programmes Java-like
- Probablement un exposé d'Arthur sur les champs "model" (30min environ, plus discussion)
- François propose un mini-exposé (dix minutes, tout compris) sur une petite généralisation de la règle anti-frame (i.e. l'état caché).
- Exposé d'Alexandre P. sur la monotonie.
- Exposé de Manuel Garnacho (en these a Verimag) sur une étude de cas qui pourrait etre abordable par nos techniques:
- Titre: Presentation d'un protocole de communication pour systeme reactif.
- Duree maximale: 30 mn (expose a mettre le jeudi apres-midi ou le vendredi matin avant 11h30).
- Exposé de Wendi sur composition de modules en Why
Participants
- Grenoble.
- Sylvain Boulmé
- Marie-Laure Potet
- Michael Perin
- Manuel Garnacho
- Pierre Corbineau
- Gallium
- Arthur Charguéraud.
- François Pottier.
- Alexandre Pilkiewicz
- pi-r2
- Yann Regis-Gianas
- Cassis
- Alain Giorgetti
- Olga Kouchnarenko
- Proval
- Claude Marché
- Wendi Urribarrí
- Johannes Kanig
- Romain Bardou
- Participation au repas du jeudi soir
- Sylvain Boulmé.
- Alain Giorgetti
- Olga Kouchnarenko
- Claude Marché
- Pierre Corbineau
- Wendi Urribarrí
- Johannes Kanig
- [Ajouter votre participation ici]
Lieu et details pratiques
Debut de la reunion le 12 mars vers 12h.
L'adresse du lieu de reunion est:
Verimag (batiment Centre Equation) 2 avenue de Vignate 38610 Gieres
Voir acces au CTL
On conseille a priori de prendre des hotels du centre ville pres de la gare. De la gare, il faut compter environ 30 minutes pour aller a Verimag en tramway (c'est direct).
Voir liste d'hotels
Réunion du 6-7 novembre 2008, Besançon
Programme approximatif
- nouvelles
- exposé Pierre Corbineau « Formaliser en Coq l'approche correct par construction : le cas du noyau de HOL-light »
- groupe de travail Hashmap
- groupe de travail Raffinement en Why
- groupe de travail Iterateurs
- sujets de stage
- questions diverses
Participants
- Proval
- Claude Marché
- Romain Bardou
- Johannes Kanig
- Wendi Urribarrí
- (Christine Paulin excusée)
- (Jean-Christophe Filliâtre excusé)
- (Yann Regis-Gianas excusé)
- Grenoble
- Sylvain Boulmé
- Marie-Laure Potet
- Pierre Corbineau
- Gallium
- Arthur Charguéraud
- (François Pottier excusé)
- Cassis
- Kalou Cabrera-Castillos
- Alain Giorgetti
- Olga Kouchnarenko
- Participants au diner du jeudi soir:
- Alain Giorgetti, Olga Kouchnarenko, Pierre Corbineau, Marie-Laure Potet, Sylvain Boulmé, [Ajouter ici votre participation]
- Exposés possibles
- Pierre Corbineau: Formaliser en Coq l'approche correct par construction : le cas du noyau de HOL-light
- Sylvain Boulmé et Marie-Laure Potet. Exemple B d'un iterateur sur une file de priorité: vers une extension de la méthode unpack/pack avec du raffinement. (Cet exposé peut rentrer dans le cadre des discussions raffinement en Why ou itérateurs).
- [Ajouter ici proposition d'exposés]
- groupes de travail possible :
- Autour de l'exemple des tableaux persistants (Interessés: Claude Marché, François Pottier, Alain Giorgetti, Kalou Cabrera-Castillos, Romain Bardou, Johannes Kanig, Arthur Charguéraud, completer)
- Liens entre CeProMi et développement Why (Intéressés : Alain Giorgetti, Claude Marché, Romain Bardou, Wendi Urribarrí, Olga Kouchnarenko, completer)
- Spécifications avec ordre supérieur et effets (Intéressés : Claude Marché, Romain Bardou, Johannes Kanig, Wendi Urribarrí, François Pottier, Arthur Charguéraud, completer)
- [Ajouter ici proposition de groupe de travail]
- Sujets divers
- Futures propositions de stages
- Futures rencontres/reunions: forme, lieu, duree ?
- Visites ponctuelles
- [Ajouter ici questions diverses]
Réunion du 12-13 juin 2008
Programme approximatif
- 12 juin
- matin: discussions diverses
- 13h: repas sur place
- 14h: questions diverses, compte-rendu sur l'action COST FVOOS, Romain Bardou : presentation des travaux sur "Regional Logic" de Naumann et al.
- 16h: groupe de travail sur l'exemple des tableaux persistants ou analogues
- 19h30: repas restaurant sur Paris
- 13 juin
- 9h30: groupe de travail sur Spécifications avec ordre supérieur et effets
- 11h: Liens entre CeProMi et développement Why
- 12h30: repas sur place
- apres-midi: discussions
Participants
- Claude Marché (local)
- Sylvain Boulmé (arrivee 11:59 Gare de Lyon, depart 16:38 Gare de Lyon, hotel ?)
- Marie-Laure Potet (arrivee 11:59 Gare de Lyon, depart 16:38 Gare de Lyon, hotel ?)
- Arthur Charguéraud (arrivée le 12 vers 10h, départ le 13 après déjeûner)
- François Pottier (arrivée le 12 entre 10h et 13h?, départ le 13 après déjeûner)
- Romain Bardou (local)
- Kalou Cabrera-Castillos (arrivée le 12 à 9h38 gare de Lyon, départ le 13 pour 14h28 gare de Lyon)
- Alain Giorgetti (arrivée le 12 à 9h38 gare de Lyon, départ le 13 pour 17h28 gare de Lyon)
- Olga Kouchnarenko (arrivée le 12 à 9h38 gare de Lyon, départ le 13 pour 17h28 gare de Lyon)
- Johannes Kanig (local)
- Wendi Urribarrí (local)
- [Ajouter ici votre participation]
- Participants au diner du jeudi soir:
- Claude Marché
- Kalou Cabrera-Castillos
- Alain Giorgetti
- Olga Kouchnarenko
- [Ajouter ici votre participation]
- Exposés possibles
- Sylvain Boulmé : exemple du crible d'erathosthene à confirmer
- Romain Bardou : presentation des travaux sur "Regional Logic" de Naumann et al. confirmé
- [Ajouter ici proposition d'exposés]
- groupes de travail possible :
- Autour de l'exemple des tableaux persistants (Interessés: Claude Marché, François Pottier, Alain Giorgetti, Kalou Cabrera-Castillos, Romain Bardou, Johannes Kanig, completer)
- Liens entre CeProMi et développement Why (Intéressés : Alain Giorgetti, Claude Marché, Romain Bardou, Wendi Urribarrí, Olga Kouchnarenko, completer)
- Spécifications avec ordre supérieur et effets (Intéressés : Claude Marché, Romain Bardou, Johannes Kanig, Wendi Urribarrí, François Pottier, completer)
- [Ajouter ici proposition de groupe de travail]
- Sujets divers
- Compte-rendu sur l'action COST [FVOOS]
- Futures propositions de stages
- Futures rencontres/reunions: forme, lieu, duree ?
- Visites ponctuelles
- [Ajouter ici questions diverses]
Réunion de lancement le 20 mars 2008
- Présents:
- Cassis: Alain Giorgetti, Olga Kouchnarenko, Christophe Ringeissen
- Grenoble: Sylvain Boulmé, Marie-Laure Potet
- Gallium: François Pottier, Arthur Charguéraud, Alexandre Pilkiewicz
- Proval: Jean-Christophe Filliâtre, Christine Paulin, Claude Marché, Romain Bardou, Johannes Kanig, Wendi Urribarri
- Programme:
- 9h15 Accueil
- 10h Wendi Urribarri : Raffinement de données en Why
- 11h15 Sylvain Boulmé : exemples invariants + partage + modules (sans alias)
- 12h30 Pause déjeuner
- 14h : Points d'organisation
- 14h45 Alain Giorgetti : B#, contexte et extension de contexte
- 15h45 : Arthur Charguéraud : Preuve de programmes ML impératifs à l'aide d'une traduction fonctionnelle dirigée par un système de types avec capacités.
- 16h45 : Claude Marché : version Java/Krakatoa de l'exemple des tableaux persistants, également disponible le code Java et le code ml
- 17h30 : fin
Réunion de « pré-lancement » le 14 février
- Présents: Alain Giorgetti, Sylvain Boulmé et les franciliens.
- Programme:
- 10h30: séminaire de François Pottier, « Effets cachés en style direct, ou: une règle d'anti-encadrement d'ordre supérieur »
- Pause déjeuner
- après-midi: réunion informelle en salle N 107
- nous discutons des Programmes exemples
