Attention: il s'agit d'un programme préliminaire susceptible d'être modifié.
| 16:30-17:30 | Accueil | |
| 17:30-19:00 | Des théories des types qui font de l'effet (partie I) | Pierre-Marie Pédrot |
| 19:00-19:30 | CAMLroot: revisiting the OCaml FFI | Frédéric Bour |
| 19:30-19:50 | Learn-OCaml : un assistant à l'enseignement d'OCaml | Çagdas Bozman, Benjamin Canou, Roberto di Cosmo, Pierrick Couderc, Louis Gesbert, Grégoire Henry, Fabrice Le Fessant, Michel Mauny, Carine Morel, Loïc Peyrot and Yann Régis-Gianas |
| 19:50 | Dîner |
| 9:00-10:00 | Types de session : état de l’art et perspectives | Ilaria Castellani |
| 10:00-10:30 | Pause | |
| 10:30-11:00 | Arguments cadencés dans un compilateur Lustre vérifié | Timothy Bourke et Marc Pouzet |
| 11:00-11:30 | Typer: ML boosted with type theory and Scheme | Stefan Monnier |
| 11:30-12:00 | Suspension et fonctorialisation : deux opérations implicites utiles en CaTT | Thibaut Benjamin et Samuel Mimram |
| 12:00-12:30 | Unboxing Mutually Recursive Type Definitions | Rodolphe Lepigre, Gabriel Scherer et Simon Colin |
| 12:30-14:00 | Déjeuner | |
| 14:00-15:30 | Activités libres | |
| 15:30-17:00 | Arithmétique des ordinateurs et preuves formelles(partie I) | Guillaume Melquiond |
| 17:00-17:30 | Pause | |
| 17:30-18:00 | Session spéciale 30 ans de JFLA : Trente ans par mers et par monts | Thérèse Hardin et Pierre Weis |
| 18:00-18:30 | Retour sur 25 ans de programmation avec OCaml | Jean-Christophe Filliâtre |
| 18:30-19:00 | Programmation Synchrone aux JFLA | Louis Mandel |
| 19:00-19:30 | Sémantiques Formelles et Certifiées | Alan Schmitt |
| 19:30 | Dîner |
| 9:00-10:00 | Les protocoles de déplacement de robots : l'algorithmique distribuée comme terrain de jeu pour la preuve formelle | Pierre Courtieu |
| 10:00-10:30 | Pause | |
| 10:30-11:00 | Formalisation en Coq d'algorithmes de filtres numériques | Diane Gallois-Wong |
| 11:00-11:30 | Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq | Charly Gries, Julien Narboux et Pierre Boutry |
| 11:30-12:00 | SQL à l’épreuve de Coq : une sémantique formelle pour SQL | Véronique Benzaken et Evelyne Contejean |
| 12:00-12:30 | SMTCoq: automatisation expressive et extensible dans Coq | Valentin Blot, Amina Bousalem, Quentin Garchery et Chantal Keller |
| 12:30-14:00 | Déjeuner | |
| 14:00-17:00 | Ballade en raquettes | |
| 17:00-18:30 | Des théories des types qui font de l'effet (partie II) | Pierre-Marie Pédrot |
| 18:30-18:50 | En finir avec les faux positifs grâce à l’exécution symbolique robuste | Benjamin Farinier, Sébastien Bardin, Richard Bonichon et Marie-Laure Potet |
| 18:50-19:10 | Formally Verified Decomposition of Non-binary Constraints into Equivalent Binary Constraints | Catherine Dubois |
| 19:10-19:30 | Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP | Raphaël Rieu-Helft |
| 19:30 | Dîner |
| 9:00-10:30 | Arithmétique des ordinateurs et preuves formelles (partie II) | Guillaume Melquiond |
| 10:30-11:00 | De l'assembleur sur la ligne? Appelez TInA! | Frédéric Recoules, Richard Bonichon, Sébastien Bardin, Laurent Mounier et Marie-Laure Potet |
| 11:00-11:30 | Combinatoire formelle avec Why3 et Coq | Alain Giorgetti, Catherine Dubois et Rémi Lazarini |
| 11:30 | Départ (repas à emporter) |