Mercredi 4 janvier

17:50-18:10 Accueil
18:10-19:40 Comment programmer en OCaml aujourd'hui (partie I) B. Canou
20:00 Dîner

Jeudi 5 janvier

09:00-10:00 Langage et outil pour la preuve d'un micro-noyau S. Lescuyer et F. Plateau
10:00-10:30 Result graphs for an abstract interpretation-based static analyzer P. Cuoq et R. Rieu-Helft
10:30-10:50 Pause
10:50-11:20 OCaLustre : une extension synchrone d'Ocaml pour la programmation de microcontrôleurs S. Varoumas, B. Vaugon et E. Chailloux
11:20-11:50 CloudLens: Un langage de script pour l'analyse de données semi-structurées G. Baudart, L. Mandel, O. Tardieu et M. Vaziri
11:50-12:20 Le coquillage dans le CoLis-mateur, Formalisation d'un langage de programmation de type shell N. Jeannerod
12:30-14:00 Déjeuner
14:00-16:40 Activités libres
16:40-17:10 Format unraveled R. Bonichon et P. Weis
17:10-17:30 Des unités dans le typeur J. Garrigue et D. Ly
17:30-17:50 Preuves taillées en biseau M. Clochard
17:50-18:10 Pause
18:10-19:40 Comment programmer en OCaml aujourd'hui (partie II) B. Canou
20:00 Dîner

Vendredi 6 janvier

09:00-10:00 Zenon D. Doligez
10:00-10:30 Prototyper un compilateur de requêtes avec Coq J. Auerbach, M. Hirzel, L. Mandel, A. Shinnar et J. Siméon
10:30-10:50 Pause
10:50-11:20 Typeful Continuations M. Puech
11:20-11:50 Modèles de la théorie des types donnés par traduction de programme S. Boulier, P.-M. Pédrot et N. Tabareau
11:50-12:20 Non-Interference through Annotated Multisemantics G. Cabon et A. Schmitt
12:30-14:00 Déjeuner
14:00-16:40 Activités libres
16:40-17:10 Vérification de la génération modulaire du code impératif pour Lustre T. Bourke, P.-É. Dagand, M. Pouzet et L. Rieg
17:10-17:30 Causalité dans les calculs d'événements B. P. Serpette et D. Janin
17:30-17:50 A refinement-based approach to large scale reflection for algebra C. Cohen et D. Rouhling
17:50-18:10 Pause
18:10-19:40 Exprimer ses théories en Dedukti, le vérificateur de preuves universel (partie I) G. Burel
19:45 Apéritif
20:15 Dîner de gala

Samedi 7 janvier

09:00-09:30 Défonctionnaliser pour prouver M. Pereira
09:30-10:00 Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe R. Chen et J.-J. Lévy
10:00-10:20 Pause
10:20-11:50 Exprimer ses théories en Dedukti, le vérificateur de preuves universel (partie II) G. Burel
12:00-13:00 Déjeuner puis départ de la navette