|
Cours et Colloques |
Contact:
symposia@inria.fr
JFLA 2004
26 et 27 janvier 2004 Sainte-Marie-de-Ré (Charente-Maritime)
Les actes en un seul fichier
le fichier compressé au format
tar
de l'ensemble des fichiers postscript des actes.
Le moyen d'imprimer facilement les actes.
Les actes fichier par fichier
Premier jour: 26 janvier 2004
- 9h Accueil - Présentation
- 9h00 - 10h00 Conférence invitée
Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve?.
Jean Goubault-Larrecq (LSV, Ens Cachan).
le postscript
- 10h - 10h30 Pause-café
- 10h30 - 11h
Ocaml-templates, génération de code à partir des types.
François Maurel (PPS, Paris 7).
le postscript
- 11h - 11h30
Typage fort et typage souple des collections topologiques.
Julien Cohen (LAMI, Évry).
le postscript
- 11h30 - 12h00
Une bibliothèque certifiée de programmes fonctionnels BSP.
Frédéric Gava (LACL, Paris 12).
le postscript
- 12h00 - 16h Déjeuner et excursion
- 16h - 16h30 Pause café
- 16h30 - 17h
Une procédure de décision réflexive pour un fragment de l'arithmétique de Presburger.
Pierre Crégut (France-Télécom R & D - DTL/TAL).
le postscript
- 17h - 17h30
Gb: une procédure de décision pour le système Coq.
Jérôme Créci (Saarbrucken), Loïc Pottier (INRIA Sophia-Antipolis).
le postscript
- 18h - 19h Table ronde: La place et la pratique du test dans la programmation fonctionnelle
Deuxième jour: 27 janvier 2004
- 9h - 10h Conférence invitée
Certification d'un compilateur: enjeux, problèmes et approches.
Xavier Leroy (INRIA Rocquencourt).
- 10h00- 10h30 Pause-café
- 10h30 - 11h00
Application du toplevel embarqué d'Objective Caml.
Clément Capel, Emmanuel Chailloux (PPS, Paris 7), Jean-Marc Eber (LexiFi SAS).
le postscript
- 11h00 - 11h30
GlSurf: maths et dessins en Ocaml.
Christophe Raffalli (Laboratoire de Mathématiques, Univ. Savoie).
le postscript
- 11h30 - 12h00
Formalisation en Coq d'un cours de géométrie pour le lycée.
Frédérique Guilhot (INRIA Sophia-Antipolis).
le postscript
- 12h00 - 13h30 Déjeuner
- 13h30 - 14h00
Évaluation de l'extensibilité de PhoX: B/PhoX un assistant de preuves pour B.
Jérôme Rocheteau, Samuel Colin, Georges Mariano, Vincent Poirriez.
le postscript
- 14h - 14h30
Algorithmes et complexités de la réduction statique minimale.
Ludovic Henrio, Bernard Paul Serpette, Szabolcs Szentes.
le postscript
- 14h30 - 15h
Programmation paramétrée en ML et automates d'architecture.
Philippe Narbel (LaBRI, Bordeaux I).
le postscript
- 15h00- 15h30 Pause-café
- 15h30 - 16h30 Démonstrations
- 16h30 Fin des Journées
Pour tout renseignement, contacter
Marie-Françoise Loubressac
INRIA Rocquencourt
Bureau des Cours et Colloques (JFLA2004)
Domaine de Voluceau - BP 105
78153 Le Chesnay Cedex
Tél.: +33 (0) 1 39 63 56 00 - Fax : +33 (0) 1 39 63 56 38
email : Marie-Francoise.Loubressac@inria.fr
http://pauillac.inria.fr/jfla/2004/
Mis à jour par Pierre.Weis@inria.fr
Powered by Caml