Mercredi 8
Jeudi 9
Vendredi 10
Samedi 11

Programme des JFLAs 2014

Mercredi 8 janvier

12h45 navette depuis St Raphaël (pour le train arrivant à 12h30)
13h00-14h00 Repas
14h30-16h00 Modélisation de programmes probabilistes en Coq (I) Christine Paulin
16h00-16h30 pause
16h30-18h00 Du calcul mathématique aux calculs informatiques (I) Slides et Exercices et un Article Olivier Danvy Venir avec son ordinateur
18h00-18h30 pause
18h30-18h40 Traduction prouvée d'HOL4 vers le premier ordre Slides Thibaut Gauthier, Chantal Keller et Michael Norrish
18h40-18h50 Le petit guide du bouturage Slides Jean-Christophe Filliâtre
18h50-19h00 Réflexions sur l'écriture de parsers binaires robustes et présentation de la solution Parsifal Slides Olivier Levillain
19h00 Repas
20h30-21h30 Communication Scientifique Slides Olivier Danvy Venir avec son ordinateur

Jeudi 9 janvier

09h00-10h30 Du calcul mathématique aux calculs informatiques (II) Slides et Exercices et Articles: danvy-AFP08.pdf - danvy-ICFP08.pdf - danvy-zerny-PPDP13.pdf - walk.pdf Olivier Danvy Venir avec son ordinateur
10h30-11h00 pause
11h00-11h30 Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières Slides Sylvain Conchon, David Declerck, Luc Maranget et Alain Mebsout
11h30-12h00 What could Coq do for Database Software ? -- A progress Report Slides Yoichi Hirai and Reynald Affeldt
12h00-12h30 Comment un chameau peut-il écrire un journal ? Slides Julien Signoles
12h45-14h00 repas
14h00-16h00 balades et discussions
16h00-17h Une sémantique pour la biologie moléculaire ? Slides Jean Krivine
17h00-17h30 pause
17h30-18h00 Formal verification in Coq of program properties involving the global state effect Slides Jean Guillaume Dumas, Dominique Duval, Burak Ekici and Damien Pous
18h00-18h30 Une sémantique statique pour MongoDB Slides Adrien Husson.
18h30-19h00 Pretty-big-step-semantics-based Certified Abstract Interpretation Slides Martin Bodin, Thomas Jensen and Alan Schmitt
19h00-20h30 repas
20h30-21h30 Solutions des exercices Slides et Solutions en WHY3 -1 et -2 et aussi en Coq -1 et -2 et encore une autre en Coq .pdf et .v Olivier Danvy

Vendredi 10 janvier

09h00-10h30 Modélisation de programmes probabilistes en coq (II) Slides Christine Paulin
10h30-11h00 pause
11h00-11h30 Analyse de dépendances et correction des réseaux de preuve Slides Marc Bagnol, Amina Doumane et Alexis Saurin
11h30-12h00 De la KAM avec un Processus d’Ordre Supérieur Slides Damien Pous et Alan Schmitt
12h00-12h30 Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseuse Slides Pierre-Marie Pédrot et Alexis Saurin
12h45-14h00 repas
14h00-16h00 balades et discussions
16h00-17h Vérification en Coq d'analyseurs statiques Slides Xavier Leroy
17h00-17h30 pause
17h30-18h00 Unification des couleurs dans un lambda-calcul polychrome Slides Bernard Serpette et Pascal Manoury
18h00-18h30 Exécution efficace de programmes ReactiveML Slides Louis Mandel et Cédric Pasteur
18h30-19h00 Réseaux de Kahn à rafales et horloges entières Slides Adrien Guatto et Louis Mandel
19h00-20h30 repas
20h30-21h00 HoTT Slides Guillaume Brunerie
21h00-21h30 Coq passe le bac Slides Catherine Lelay

Samedi 11 janvier

09h00-9h30 ReactiveML, un langage de programmation réactif Slides Louis Mandel et Marc Pouzet. 25 ans - JFLA05
09h30-10h00 Union-Find Persistant Slides 2013 et Slides 2007 et Slides 2008 Sylvain Conchon et Jean-Christophe Filliâtre. 25 ans - JFLA07
10h00-10h30 pause
10h30-11h00 Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes. Slides Sandrine Blazy, Benoît Robillard et Éric Soutif. 25 ans - JFLA08
11h00-11h30 Calcul de plus faible précondition, revisité en Why3. Slides Claude Marché et Asma Tafat. 25 ans - JFLA13
11h30-12h00 bilan des journées
12h-13h30 repas
13h45 navette pour St Raphaël (pour le train partant à 14h30)