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 SupeÌ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) | ||