Logo JFLA 2019

Programme

Nous avons deux cours invités (durant chacun trois heures, en deux parties d'une heure et demi) ainsi que deux exposés invités d'une heure chacun. La durée des présentations est de vingt-cinq minutes pour les articles longs et de quinze minutes pour les articles courts.

Attention: il s'agit d'un programme préliminaire susceptible d'être modifié.

Mercredi 30 janvier 2019

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

Jeudi 31 janvier 2019

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 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 Alain Schmitt
19:30 Dîner

Vendredi 1er février 2019

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 Activités libres
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

Samedi 2 février 2019

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)