Programme des Journées
Jeudi 21 Novembre 1996 (journée plénière)
8h30-9h00 : Accueil
9h00-10h30 : session programmation fonctionnelle
Objective ML. Didier Rémy et Jérôme Vouillon INRIA-Rocquencourt (ML)
Automatisation de la stratégie des accumulateurs par les systèmes de réécriture "épluchés". Françoise Bellegarde, Stéphane Varnier, LIB, Univ. Besançon (TFTP).
Grammaires Attribuéés et Folds: Opérateurs de Contrôle Génériques. E. Duris, D. Parigot, G. Roussel, M. Jourdan (pôle Interfaces et Environnements, Minotaur)
10h30-11h00 : pause
11h00-12h00 : session programmation parallèle et distribuée (Ch. Queinnec)
Parallélisation de boucles sisal: génération de pipelines. I. Attali, D Caromel, R Guider, A Wendelborn
Un modèle orienté objet pour la synchronisation et la configuration d'applications réparties. JP Bahsoun, L Feraud, JF Pouilly, JC Sakdavong
12h00-13h30 : déjeuner
13h30-14h00 : démonstrations
14h00-14h30 : session programmation parallèle et distribuée (suite)
Les amalgames: un mécanisme pour la structuration et la construction
incrémentale de programmes déclaratifs. O. Michel
14h30-16h00 : session programmation objet (Ch. Dony)
Satisfaction de contraintes et programmation par objets. Francois Pachet (LAFORIA)
OQUAL : un langage commun pour les assertions et les requ^etes basé sur Eiffel Ph.Collet (I3S)
Compréhension de la délégation, application aux objets morcelés. D.Bardou (LIRMM)
16h00-16h30 : pause
16h30-18h00 : session contraintes et programmation logique (Ph. Devienne)
Preuve de terminaison par résolution de contraintes d'ordre sur une structure partagée. Thomas Genet et Isabelle Gnaedig, CRIN/INRIA (DEMETHEO)
Slicing pour programmes Prolog. S. Schoenig et M. Ducasse, Rennes (LANDE)
Programmes concurrents par contraintes et logique linéaire non-commutative. P. Ruet, F. Fages, LIENS, Paris (SCALP/GASP)
18h30-19h30 : réunion de l'équipe de direction élargie sur l'avenir du GDR PROGRAMMATION.
Vendredi 22 novembre 1996 (journée plénière)
8h30-10h30 : session interfaces et environnements (I. Attali)
Manipuler les graphes avec Cabri-graph. Y. Carbonneaux, J.-M. Laborde, M. Madani (MC2)
Un langage objet pour la construction d'interfaces graphiques. E. Gallesio (CISe)
Les trois services du noyau sémantique indispensables a l'IHM. J-D. Fekete (ISIS)
TrFl: un langage de description de transformations. I. Attali et C. Roudet (Minotaur)
10h30-11h00 : pause
11h00-11h30 : session contraintes et programmation logique (Ph. Devienne)
Ensembles intentionnels par les substitutions explicites. G. Richard, F. Saubion et A. Tellez-Arenas, Orleans (SCALP/CQFD)
11h30-12h00 : session preuves et spécifications algébriques (Ch. Paulin)
De la décidabilité de l'unifiabilité dans les systèmes de réécritures. Sebastien Limet et Pierre Rety, Orleans (CQFD)
12h00-13h30 : déjeuner
13h30-14h00 : démonstrations
14h00-14h45 : conférence invitée Yves Caseau, Directeur de Recherche chez Bouygues
CLAIRE: Un language pour résoudre des problèmes d'optimisation combinatoire par propagation de contraintes :
Cet exposé présente l'application de la programmation par contrainte à un certain nombre de problèmes d'optimisation combinatoire, classiques tels que l'ordonnancement ou les tournées, ou plus originaux, tels que ceux que nous avons traité chez Bouygues. Nous montrons comment des algorithmes hybrides, combinant des techniques de propagation avec d'autres méthodes nous ont permis d'obtenir des résultats satisfaisants (compétitifs). Nous présentons ensuite le langage CLAIRE, qui nous sert à implémenter ces algorithmes hybrides de facon efficace ET élégante.
15h00-16h30 session preuves et spécifications algébriques (suite)
Vérification d' un modèle de procédé de développement. Xavier Crégut, Bernard Coulette (ADER)
From incomplete proofs to incomplete lambda-terms in Type Theory. C. Munoz (COQ)
Spécification algébrique et sortes ordonnées pour un multi-modeleur déxtensions de cartes. Yves Bertrand et Pascal Lienhardt (SAGACE)
Graphes PATCH: une structure de données pour la complétion efficace des groupes finiment présentés. Christopher Lynch, Polina Strogova, Nancy (DEMETHEO)
Travailler avec des ensembles infinis de termes représentés par des termes iterés. A.Amaniss, M.Hermann, D. Lugiez, Nancy (DEMETHEO)
Filtrage d'ordre supérieur et automates. H. Comon et Y. Jurski, Orsay (DEMETHEO)
La recherche de cycles pour la compilation logique. O. Roussel et P. Mathieu, Lille (SCALP).
Une caractérisation des arbres SLD en programmation logique avec contraintes A. Tessier, Orleans (SCALP)
Induction de programmes logiques avec contraintes. L. Martin et C. Vrain, Orleans (SCALP).
CSP continu et consistance locale. F. Benhamou et L. Granvilliers, Orleans (SCALP).
Une sémantique operationnelle pour la relaxation de contraintes. P. Boizumault, Nantes (SCALP).
Titre à préciser JL. Imbert, Clermont-Ferrand (SCALP).
Boosting the Interval Narrowing Algorithm. O. Lhomme, A. Goetlib, M. Rueher, P. Taillibert (SCALP).
Engineering Transformations of Attributed Grammars in LambdaProlog. Olivier Ridoux, Rennes (LANDE).
Parametric Polymorphism for Logic Programming. P. Louvet et O. Ridoux, Rennes (LANDE).
Outils de navigation et de maintenance dans un script de preuve. O. Pons (Minotaur)
Généricité dans les Grammaires Attribuées. Loic Correnson (Minotaur)
Serveur www pour Calico. Maylis Delest (MC2)
Logique et Synthèse de Programmes Impératifs. P. Bellot, J.-P. Cottin, A. Demaille, J. Leneutre, D. Sarni, E. Zarpas (ADER)
Assistance à la preuve de programmes UNITY à l'aide du démonstrateur COQ. X. Thirioux, G. Padiou (ADER)
Procédures de décision dans les systèmes avec types dépendents. Samuel Boutin (COQ)
Arbres de Boehm et Lustre. H. Laulhere (COQ) Un calcul de modules pour Coq. J. Courant (COQ)
Preuve de théorèmes dans les théories de Horn avec des Algèbres prédéfinies. N. Andrianarivelo, W Bousdira, J. Chabin (CQFD)
Modélisation et preuve d'architectures distribuées avec le démonstrateur de Boyer-Moore. Laurence Pierre (CQFD)
Spécifications algébriques avec état implicite. C. Khoury (SAGACE)
Introduction du temps réel dans les spécifications algébriques avec états. Stefan Beroff, Marc Aiguier (SAGACE)
Sur le test probabiliste de formules et ses applications au test de logiciel. Pascale Le Gall, Laurent Bouaziz et Gilles Bernot (SAGACE)
Une méthode de retro-ingénierie utilisant les spécifications algébriques. Christine Choppy et Sophie Cherki (SAGACE)
Dérivation de systèmes de réécriture pour construire efficacement des subdivisions planes. Jean-François Dufourd et David Cazier (SAGACE)
Ajout de conditionnelle dans un système de modulesà la Caml Special Light. Francois Pessaux, INRIA-Rocquencourt (ML).
Inférence de types pour le $\pi$-calcul polyadique avec relation de sous-typage. Mina Abdiche, LRI, Univ. Paris 11 (ML).
Simulation des systèmes forward-branching par des systèmes constructeurs. Bruno Salinier, Robert Strandh, LaBRI, Univ. Bordeaux I
L'approche Berry-Curien des langages fonctionnels: application au parallélisme en processus statiques. Gaétan Hains, LIFO, Univ. d'Orléans.
Dépendances interobjets et sémantique formelle. M.Blay (U.Nice)
Utiliser les objets pour la programmation // et répartie - Synthèse. J.P.Briot (LAFORIA)
Compilation de la liaison dynamique des langages de classes.
Le compilateur SmallEiffel. D.Colnet (CRIN)
DIMA : un environnement de conception et de réalisation de systèmes multi-agents. Z. Guessoum (Laforia)
Description de NeoClasstalk. Frederic Rivard (Ecole des Mines de Nantes)
Méta-manipulations en génie logiciel. R.Rousseau (I3S)
Application du cadre de conception modulaire d'objets CROME à Smalltalk Gille Vanwormhoudt (LIFL)
Le contrôle de type en objet: le noeud problème et des solutions. J.C.Royer (IRIN)
Déduction Automatique avec Contraintes en DATAC. Laurent Vigneron, Nancy (DEMETHEO)
Prelog, un processeur Prolog. G. Canet et K. Musumbu, Bordeaux (GASP)
Using CalICo for interactive books. M. Delest, J. M. Fedou, Bordeaux (MC2)
Scilab et Metanet: calcul sur les graphes et les réseaux. C. Gomez et M. Goursat (MC2)
Manipuler les graphes avec Cabri-graph. Y. Carbonneaux, J.-M. Laborde, M. Madani (MC2)
Interfaces graphiques en Scheme. E. Gallesio (CISe)
Outils de navigation et de maintenance dans un script de preuve. O. Pons (Minotaur)
Compilation du filtrage avec types dépendents. C. Cornes, COQ
A new proof manager and graphic interface for the larch prover. Frédéric Voisin, SAGACE
Déductions dans les théories de Horn avec Algèbres prédéfinies. N. Andrianarivelo, W Bousdira, J. Chabin, CQFD