La construction d'une théorie modulo pour la théorie de Zermelo-Fraenkel passe par la compréhension de la construction de réaliseurs pour les axiomes de cette théorie. Nous présentons donc une manière de réaliser les axiomes de IZF, une présentation intuitionniste de la théorie des ensembles. Ceci consiste à associer un lambda terme à chaque axiome de la théorie et à chaque axiome logique (pour la présentation de hilbert). Nous construisons alors un modèle de réaliseurs, et prouvons la consistance de IZF grace à ce modèle.

Nous avons expliqué l'architecture générale des prouveurs basés sur la résolution puis rappellé certaines techniques utilisées pour réduire le non-déterminisme lié à l'application de la règle de résolution. En particulier nous avons présenté la résolution avec ensemble de support et la résolution ordonnée avec sélection, en insistant sur les conditions qui permettent de conserver la complétude réfutationnelle. Nous avons vu qu'en combinant ces deux dernières techniques, on peut perdre la complétude réfutationnelle. Après avoir rappelé le rapport de cette combinaison avec la résolution modulo polarisé, nous avons montré que sa complétude est équivalente avec l'admissibilité des coupures en déduction modulo.

Ces idées ont été appliquées afin d'obtenir facilement une extension d'un prouveur existant basé sur la résolution. En effet, la plupart des prouveurs utilise une boucle dite boucle d'Otter qui permet de contrôler quelles clauses doivent être résolues. Cette boucle provient de la résolution avec ensemble de support. De plus, les prouveurs actuels utilisent possède également des mécanisme de sélection des littéraux dans les clauses. Nous avons donc modifié iprover (http://www.cs.man.ac.uk/~korovink/iprover/) pour qu'il fasse de la résolution avec ensemble de support et fonction de sélection. Néanmoins, il manque encore la possibilité de faire de l'unification équationnelle pour vraiment avoir de la résolution modulo polarisée. Cet ajout ne semble pas trivial, du fait de l'utilisation dans les prouveurs existants d'index pour améliorer l'unification.

Nous avons tout d'abord rappelé les règles de lambda-Pi et de lambda-Pi-modulo. Nous avons ensuite montré l'intérêt de compiler les problèmes de vérification de types: dans le contexte de lambda-pi-modulo la règle de conversion peut être très coûteuse en temps calcul, et ce d'autant plus quand les règles de réécriture sont nombreuses et complexes.

Nous avons ensuite présenté Europa. Europa est écrit en Haskell et l'architecture s'articule ainsi:

Europa est en réalité un méta vérificateur de types - il génère un vérificateur de types spécialisé au module europa donné.

Nous avons présenté les nouvelles méthodes de constructions de modèles pour la déduction modulo par l'utilisation de morphismes d'algèbres de valeurs de vérité.
Ces techniques ont permis l'élaboration d'un critère sémantique correct et complet pour la normalisation forte des théories exprimées en déduction modulo minimale.
Le principe étant le suivant :

• Construire une algèbre des candidats de réductibilité bien typés pour une théorie donnée telle que le fait d'avoir un modèle valué sur cette algèbre est un critère complet pour la normalisation forte.
• Puis construire un morphisme envoyant chacune de ces algèbres vers une nouvelle algèbre C' (que l'on a choisie correcte). Ainsi, dès qu'une théorie est fortement normalisante, elle a un modèle de candidats bien typés qui est lui-même envoyé vers un modèle à valeurs dans C'.

Etendre la déduction modulo au cadre de la logique linéaire a plusieurs attraits. C'est par exemple la meilleure porte d'entrée pour l'étude du focusing ou bien celle des réseaux de preuve étendus au formalisme de la déduction modulo. C'est ce dernier point qui a été abordé en particulier et qui pourrait permettre de mieux appréhender plusieurs concepts dans le cadre du calcul des séquents classique et/ou intuitioniste:

• la notion de candidat de réductibilité, en vue d'étendre des résultats de Super-Cohérence
• la définition de termes de preuve

Les calculs des séquents classique sont des systèmes déductifs qui présentent de nombreux avantages. Leur utilisation est simple, ils sont facilement extensibles et de nombreuses procédures de recherche de preuve dérivent de ces systèmes. Parmi les extensions intéressantes de tels systèmes, on peut trouver le focusing, la méthode des tableaux, la méthode inverse, la definitional reflection, la (sur)déduction modulo. Ces extensions fournissent des avancées substantielles à la machinerie déductive. Ces systèmes présentent aussi un intérêt pour les programmeurs à travers les analogies formules/types comme par exemple la correspondance de Griffin entre la logique classique et la programmation CPS.

Néanmoins, la flexibilité des calculs des séquents classiques se repercute aussi sur le large spectre de procédure d'élimination des coupures imaginables pour ces systèmes. Alors que dans le cadre de la déduction naturelle, la beta-réduction du lambda-calcul se pose naturellement comme l'élimination des coupure, il existe différentes versions de l'élimination des coupures en calcul des séquents (par exemple le lambda-bar-mu-mu-tilde calcul de Herbelin ou bien l'élimination des coupures de Urban) et elles n'admettent pas forcément les
propriétés de confluence et de normalisation forte.

Cet exposé présente l'approche récente de Lamarche et Strassburger qui propose une représentation des preuves en calcul des séquents classique sous la forme de réseaux de preuve. En particulier les coupures sont des connecteurs logiques. L'élimination des coupures définie alors sur ces réseaux est fortement normalisante et confluente.

L'évaluateur de Haskell trouve des formes normales de tête faible: nécessite d'avoir de la normalisation par évaluation. Problème avec les grosses conversions (ex: fib 32 = fib 32) ou l'on ne veut pas commencer par normaliser. Remarque de Gilles: définitions opaques/transparents, comme dans la machine de Coq pour ``forcer'' la conversion seulement si l'utilisateur en a besoin. Autres limitations:

• besoin de règles de réécriture orthogonale (ou alors accepter stratégie de sélection fixe top-down)
• Rajout de l'associatif-commutatif difficile
• réductions inutiles
• génération un programme fonctionnel qui doit être parsé ensuite est lourd
• temps de compilation souvent plus élevé que temps du test de conversion. Stratégie ``Just in Time'' pour compiler efficacement le code seulement lorsqu'on en a besoin (JVM/LLVM).

Solution: compiler vers un langage plus bas niveau, permettant plus de contrôle. Il faut donc simplifier nos termes.

Défonctionalisation: transformer des fonctions en structures de données: au lieu de passer des fonctions en argument, on va pouvoir passer les structures de données.

Par ailleurs, passage en CPS avant la défonctionalisation. Avantages:

• tous les redex sont a la tete du terme.
• correspondance directe avec SSA, qui se trouve être la forme nécessaire des programmes exécutables sur LLVM, qui est une
  architecture de compilation et d'optimisation puissante.
  

En Déduction Naturelle modulo, la réécriture est interprétée silencieusement: si A est équivalent à B, et si t est de type A, alors il est aussi de type B. C'est en particulier visible dans la déduction naturelle avec règles fold/unfold.

Cette interprétation est justement la source du "paradoxe" suivant: il est possible de trouver des systèmes de réécriture qui possèdent la propriété d'élimination des coupures, mais où l'on peut typer des termes de preuve qui ne normalisent pas.

C'est pourquoi il est parfois nécessaire de raffiner cette interprétation et d'assigner un lambda-terme spécifique à chaque réécriture. La question qui reste en suspens est: comment automatiser ceci ? Plusieurs pistes d'étude sont envisageables, en particulier la complétion abstraite de Burel et Kirchner ou bien les méthodes de complétude sémantique.

Lemuridae, à l'origine un assistant de preuve pour la superdéduction, est maintenant plutôt un typechecker/interpréteur pour diverses logiques (et calculs associés) du premier ordre: fold, superdéduction, modulo, terms d'Urban, lambda-mu. Il propose aussi une traduction des démonstrations vers les proofterms coq.

Plusieurs pistes ont été évoquées quand à son utilité ou son avenir:

• Traduction d'Europa vers Lemu
• Traduction de Lemu vers Europa
• Investiguer les aspects classiques de l'assistant

Plusieurs pistes ont été évoquées encoder les types inductifs dans Europa

• À la Parigot (papier Lisa et Paul): les règles de réécritures sur les types (nat,list,etc.) permettent le typage de termes qui encodent les constructeurs et dont le comportement calculatoire simule celui du récurseur habituellement associé.
• En encodant un certain nombre de primitives comme Sigma et W, qui permettent eux-mêmes d'encoder tous les types inductifs.
• En rajoutant une constante par schéma d'élimination (le rec), et en lui associant une règle de réduction.

La normalisation par évaluation peut être un outil très puissant pour démontrer qu'une théorie modulo a la propriété de normalisation. En particulier parce qu'elle a un lien direct avec la Super-Cohérence, à la suite des travaux de Dowek et Hermant.
Cependant, les liens entre ces découvertes et la normalisation par évaluation telle qu'elle est partiquée ailleurs (Coquand, Schwichtenberg ou encore Altenkirch et al.) n'ont pas encore été défrichés. D'un côté, on a des Algèbres de Heyting et de l'autre des Structures de Kripke et des catégories. Or, ces deux sémantiques sont liées (voir par exemple Troelstra-van Dalen), à un niveau d'intrication cependant moindre que celui qui est nécessaire ici.

Les travaux fournis ont porté principalement sur la compréhension des mécanismes de normalisation par évaluation à base de Structures de Kripke catégoriques, ce qui est un préliminaire au reste du programme.