Room 206 et BBB (code d'accès 506793)
10 juin 2021 - 15h00
[FormalProofs] Petites inversion et récursion débridée en Coq, la méthode de Braga
par Jean-François Monin de Verimag
Résumé : Comment raisonner en Coq sur des fonctions récursives dont la terminaison n'est pas gagnée d'avance ? Voire sont manifestement partielles, avec un domaine de définition complexe ou même inconnu ? Comment les écrire sous forme de fonctions Coq qui à l'extraction donnent exactement le programme OCaml attendu ?
La méthode de Braga, initalement présentée par D. Larchey-Wendling et l'orateur à Braga (Types'18) répond positivement à ces questions. L'exposé se concentre sur un ingrédient clé : la récupération d'une composante structurellement décroissante dans un type inductif dépendant, écrite de façon claire et lisible.
Pour cela il a fallu faire évoluer de la technique des petites inversion qui avait été introduite pour effectuer des raisonnements intensifs basés sur une sémantique opérationnelle de CompCert et, encore à ce jour, gère des situations hors de portée de la tactique standard.
L'exposé comportera un première partie très introductive, puis une seconde partie plus spécialisée.
Pour toutes infos supplémentaires contacter directement Jean-François Monin.
