Dimanche 3 février | ||
| 15h00 | navette depuis Modane (pour le train arrivant à 14h40) | |
| 16h00-17h30 | Tester les modèles mémoire faibles en pratique | Luc Maranget |
| 17h30-18h00 | pause | |
| 18h00-18h30 | Réactivité des systèmes coopératifs: le cas de ReactiveML | Louis Mandel et Cédric Pasteur |
| 18h30-19h00 | Concurrence légère en OCaml: muthreads | Christophe Deleuze |
| 19h00-19h30 | Une analyse formelle en Coq d'un algorithme distribué probabiliste résolvant le problème du rendez-vous | Allyx Fontaine et Akka Zemmari |
| 20h00- | repas | |
Lundi 4 février | ||
| 09h00-10h30 | Programmation XML, de la théorie aux outils | Kim NguyỠn |
| 10h30-11h00 | pause | |
| 11h00-11h30 | Elaborating Inductive Definitions | Pierre-Evariste Dagand et Conor McBride |
| 11h30-12h00 | Un lambda-calcul atomique | Tom Gundersen, Willem Heijltjes et Michel Parigot |
| 12h00-12h30 | Normal Forms for the Algebraic Lambda-Calculus | Michele Alberti |
| 12h45-14h00 | repas | |
| 14h00-17h00 | neige | |
| 17h00-17h30 | Calcul de plus faible précondition, revisité en Why3 | Claude Marché and Asma Tafat |
| 17h30-18h00 | Vérification de systèmes paramétrés avec Cubicle | Sylvain Conchon, Alain Mebsout et Fatiha Zaidi |
| 18h00-18h15 | pause | |
| 18h15-18h30 | Formalisation en Coq des systèmes de calculs locaux | Pierre Castéran, Vincent Filou et Allyx Fontaine |
| 18h30-18h45 | Behaviour recognition for complex systems | Carle Patrice, Christine Choppy, Romain Cyril Kervarc et Ariane Piel |
| 18h45-19h00 | Collaboration d'analyses statiques et dynamiques avec Frama-C | Julien Signoles |
| 20h00- | repas | |
Mardi 5 février | ||
| 09h00-10h30 | Introduction à la réalisabilité classique (I) | Alexandre Miquel |
| 10h30-11h00 | pause | |
| 11h00-11h30 | combine: une bibliothèque OCaml pour la combinatoire | Jean-Christophe Filliatre et Rémy El Sibaïe |
| 11h30-12h00 | Anti-Unification with Type Classes | Nicolas Tabareau, Ãric Tanter et Ismael Figueroa |
| 12h00-12h30 | Matrices à blocs et en forme canonique | Guillaume Cano et Maxime Dénès |
| 12h45-14h00 | repas | |
| 14h00-17h00 | neige | |
| 17h00-17h45 | Langages et sécurité - généralités et cas des langages fonctionnels. (Exemples) | Olivier Levillain |
| 17h45-18h30 | LAFOSEC: Etude et comparaison de OCaml, F# et Scala du point de vue de la sécurité. | Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek |
| 18h30-18h45 | pause | |
| 18h45-19h45 | LAFOSEC: Recommandations pour les développeurs Ocaml, présentation de l'application réalisée, perspectives d'évolution de OCaml pour répondre aux besoins de sécurité | Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek |
| 20h00- | repas | |
Mercredi 6 février | ||
| 09h00-10h30 | Introduction à la réalisabilité classique (II) | Alexandre Miquel |
| 10h30-11h00 | pause | |
| 11h00-11h30 | A Certified JavaScript Interpreter | Martin Bodin et Alan Schmitt |
| 11h30-12h00 | OCamlCC -- Traduire OCaml en C en passant par le bytecode | Michel Mauny et Benoit Vaugon |
| 12h00-12h30 | Un régime au concentré d'automate | Pierre-Marie Pédrot |
| 12h45-14h00 | repas | |
| 14h00-15h30 | neige | |
| 15h30 | navette pour Modane (pour le train partant à 16h26) | |