Modules in type theory with generative definitions
Jacek Chrza̧szcz · OpenGrey (Institut de l'Information Scientifique et Technique) · 2004
Dans la thèse on présente un système de modules pour l'assistant à la démonstration Coq (développé par l'INRIA et l'Université de Paris-Sud). Le système de modules ressemble à celui utilisé dans des langages de programmation fonctionnelle comme SML ou Ocaml. Les résultats théoriques de la thèse garantissent la consistence logique de Coq étendu par les modules. La garantie couvre également le futur extention prévu du formalisme logique de Coq -par la possibilité de définir des fonctions par des règles de réécriture. Plus précisement, la thèse donne une définition d'un système de types comprenant un système des types pur (PTS), les définitions génératives telles que les types inductifs et les définitions par réécriture, et le système de modules. On montre que l'introduction des modules est correcte du point de vue logique: si le PTS donné avec des définitions génératives est consistant alors le système étendu par les modules est consistant également. Similairement, on montre que la décidabilité du système de base implique la décidabilité du système avec des modules. Le système de modules considéré a été implanté dans la version 7.4 de Coq, publié en février 2003. Dans la thèse, outre la partie théorique, on décrit les plus importantes modifications du système Coq résultant de l'implantation des modules. En particulier on présente des nouveaux mécanismes génériques pour traiter les éléments extra-logiques de Coq, comme des bases de données pour les tactiques automatisées, règles de parsing et pretty-printing défini par l'utilisateur, etc. L'utilité des modules pour représenter des théories paramétriques d'une manière commode et élégante a été confirmée par un certain nombre d'exemples intéressants.