TypiCal

Le CCI/Presburger est une variante du Calcul des Constructions Inductives intégrant au sein de sa conversion (le fragment de Hoare de) l'arithmétique linéaire entière.

Après une brève présentation de CCI/Presburger, je présenterai mon implémentation de ce calcul au sein du système Coq, notamment en soulignant les modifications apportées au noyau.

J'aborderai également le problème de la confiance en un tel noyau, via l'utilisation de procédures de décisions certifiées ou générant des certificats. En particulier, je parlerai de la décision certifiée et efficace des arithmétiques linéaires entière et rationnelle.