. Mécanisme-léger-de-preuve-déclarative,

, ? pierre angulaire de la mécanisation des jeux Preuves via calcul ? générer les conditions de vérification pour le langage dédié W ? preuve par réflexion : multiplication matrices de Strassen

, Méthode pour une classe particulière de débordements entiers

, ? absence de débordement avant 2 64 étapes de calcul, vol.37, p.38

, Perspectives Mise en pratique : ? implémenter la «preuve par débogage» dans un outil ? principalement automatiser la génération de CONT

, ? mécaniser la preuve de compilateur effectuée sur papier Problèmes ouverts : ? nécessité de la mémoire pour les stratégies ? ? extension du théorème de transfert pour les jeux ? ? pour l'

, Au sujet du non-déterminisme

, Remarque : S et/ou C peuvent être non-déterministes ? décisions non-déterministes potentiellement mal corrélées ? de même pour les exécutions

, Solution : contrôler les décisions non-déterministes pour S ? garder STEP C tel quel ? récupérer ces décisions à travers now C ? passer ces décisions comme un argument à STEP S

, Le rôle du non-déterminisme change le type de résultat que l'on peut obtenir, vol.39, p.38

, Autres contributions : débordements arithmétiques

, Méthode pour une classe particulière de débordements entiers

, ? taille collection, rangs union-find, hauteurs AVL

?. Idée, pas assez de temps pour qu'il y ait un débordement ? les entiers augmentent d'au plus 1 par unité de temps ? entiers 64 bits, unité de temps 1 ns : ? 584 ans Garanti par typage : type peano = private { v: int } val zero val succ