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 |
Copyright © 1996–2016 Inria, tous droits réservés.
