Mercredi 27 janvier

16:00-16:30 Accueil
16:30-17:00 Pendulum: une extension réactive pour la programmation Web en OCaml Rémy El Sibaïe et Emmanuel Chailloux
17:05-17:35 An Abstract Separation Logic for Interlinked Extensible Records Martin Bodin, Thomas Jensen et Alan Schmitt
17:40-18:10 Weak memory models using event structures Simon Castellan
19:30 Dîner

Jeudi 28 janvier

09:30-10:30 Construction of invariance proof methods Patrick Cousot
10:30-11:00 Pause
11:00-12:30 Une introduction à la preuve de sécurité formelle avec le système EasyCrypt (partie I) Pierre-Yves Strub
12:30-14:00 Déjeuner
14:00-16:00 Ballades et discussions
16:00-16:30 Une mesure ordinale pour les preuves de terminaison en Coq Pierre-Léo Bégay, Pascal Manoury et Itsaka Rakotonirina
16:35-17:05 Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq Charly Gries, Pierre Boutry et Julien Narboux
17:10-17:30 Présentation de la plateforme edukera Benoit Rognier and Guillaume Duhamel
17:30-18:00 Pause
18:00-19:30 Une introduction à la preuve de sécurité formelle avec le système EasyCrypt (partie II) Pierre-Yves Strub
20:00 Dîner

Vendredi 29 janvier

09:30-10:30 The global sequence protocol: a memory model for distributed systems Jonathan Protzenko
10:30-11:00 Pause
11:00-12:30 Session types and their applications (part I) Nobuko Yoshida
12:30-14:00 Déjeuner
14:00-16:00 Ballades et discussions
16:00-16:30 Reachability and error diagnosis in LR(1) automata François Pottier
16:35-17:05 Itérer avec confiance Jean-Christophe Filliâtre et Mário Pereira
17:10-17:30 Coq a dit : fromage tranché ne peut cacher ses trous Jean-Christophe Léchenet, Nikolai Kosmatov et Pascale Le Gall
17:30-18:00 Pause
18:00-19:30 Session types and their applications (part II) Nobuko Yoshida
20:00 Dîner

Samedi 30 janvier

09:30-10:00 Pour un raffinement spatio-temporel tuilé Simon Archipoff et David Janin
10:05-10:35 Sous le capot du MOOC OCaml Benjamin Canou, Çagdas Bozman et Grégoire Henry
10:40-11:00 Une preuve est une histoire Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, et Maria-Virginia Aponte
11:00-11:30 Pause, puis départ navette