Détails sur le séminaire

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.

Contact | Plan du site | Site réalisé avec SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1757487