Mercredi 7 janvier

16:30-18:00 Programmation web en Hop (I) Manuel Serrano
18:15-18:25 Analyse statique de consommation mémoire pour un langage fonctionnel/impératif typé Jérémie Salvucci et Emmmanuel Chailloux
18:25-18:35 Inférence de types nullables Michel Mauny et Benoit Vaugon
18:35-18:45 A Type-Sensitive Dependency Analysis for Algebraic Data Types and Arrays Oana Fabiana Andreescu
19:00 Dîner

Jeudi 8 janvier

9:00-10:30 Programmation web en Hop (II) Manuel Serrano
10:30-11:00 Pause
11:00-12:30 Vérification d'algorithmes distribués (I) Stephan Merz
12:30-14:00 Déjeuner
14:00-14:30 Decidability of Identity-free Relational Kleene Lattices Paul Brunet and Damien Pous
14:30-14:40 Mêler combinateurs et BNF pour l'analyse syntaxique en OCaml Rodolphe Lepigre et Christophe Raffalli
14:40-14:50 Retour d'expérience : développer une IHM lourde dans un client léger avec Js_of_ocaml David Maison et Benjamin Monate
14:50-15:00 Hybrid representation of a bio-molecular system in the Kappa Language Pierre Boutillier et Jean Krivine
15:15-15:45 Flux média tuilés polymorphes : une sémantique opérationnelle en Haskell Théis Bazin et David Janin
15:45-16:15 Mergeable persistent data-structures Benjamin Farinier, Thomas Gazagnaire and Anil Madhavapeddy
16:15-16:45 ocp-memprof: un profileur mémoire pour OCaml Çagdas Bozman, Grégoire Henry, Fabrice Le Fessant, Michel Mauny et Mohamed Iguernelala
16:45-17:15 Pause
17:15-17:45 Rester statique pour devenir plus rapide, plus précis et plus mince Arvid Jakobsson, Nikolai Kosmatov et Julien Signoles
17:45-18:15 Gagnez sur tous les tableaux Richard Genestier, Alain Giorgetti et Guillaume Petiot
18:15-18:45 Au temps en emporte le C Steven De Oliveira, Virgile Prevosto et Sébastien Bardin
19:00 Dîner

Vendredi 9 janvier

9:00-10:30 Vérification d'algorithmes distribués (II) Stephan Merz
10:30-11:00 Pause
11:00-11:30 Depth-First Search and Strong Connectivity in Coq Francois Pottier
11:30-12:00 Graphes et couplages maximaux en Coq Catherine Dubois, Sourour Elloumi, Benoit Robillard et Clément Vincent
12:00-12:30 HOCore in Coq Martin Escarrá, Petar Maksimović and Alan Schmitt
12:30-14:00 Déjeuner
14:00-15:00 Relational verification of Differential Privacy and Mechanism Design Marco Gaboardi
15:15-15:45 La stratégie de la fourchette Simon Castellan
15:45-16:15 Higher-Order Trees are Circularly Computable Jérome Fortier
16:15-16:45 Normalization by realizability also evaluates Pierre-Evariste Dagand et Gabriel Scherer
16:45-17:15 Pause
17:15-17:25 Extended abstract: simply-typed lambda calculi modeled with finite vector spaces Benoît Valiron et Steve Zdancewic
17:25-17:35 Dedukti in a Nutshell Ronan Saillard
17:35-17:45 CDuce: cohabitation of parametric, subtyping, and ad hoc polymorphism Julien Lopez
17:45-18:15 Des preuves formelles en Coq du théorème de Thalès pour les cercles David Braun et Nicolas Magaud
18:15-18:45 A linearization technique for multivariate polynomials using convex polyhedra based on Handelman's theorem Alexandre Maréchal and Michaël Périn
19:00 Dîner

Samedi 10 janvier

9:30-10:30 Verification techniques for GPU kernels Alastair Donaldson
10:30-11:00 Pause
11:00-11:30 Static conflict detection for a policy language Alix Trieu, Robert Dockins and Andrew Tolmach
11:30-12:00 Double WP: vers une preuve automatique d'un compilateur Martin Clochard et Léon Gondelman
12:00-12:10 Preuve formelle d'isolation mémoire dynamique à base de MMU Narjes Jomaa, David Nowak, Gilles Grimaud et Julien Iguchi-Cartigny
12:10-12:20 Extraction de programmes parallèles avec une bibliothèque Coq vérifiée pour le paradigme Générer-Tester-Aggréger Kento Emoto, Frédéric Loulergue et Julien Tesson
12:30-14:00 Apéritif + déjeuner
15:00 Départ navette