Si les symboles sont mal affichés sur votre navigateur voyez cette version: en texte pur.

Représentation d'algèbres non libres en théorie des types

Introduction

L'étude des fondements des mathématiques a-t-elle une autre utilité qu'occuper l'esprit de quelques mathématiciens philosophes? Autant l'intérêt pratique des mathématiques est une évidence depuis des millénaires, autant celui de la méta-mathématique n'est quant à lui apparu que récemment. Quel besoin en effet l'ingénieur a-t-il de se soucier de la justification mathématique des différentes théories qu'il utilise? La seule chose importante est que ces outils mathématiques lui permettent de construire des ponts solides. « Pourquoi n'ai-je jamais pu tirer deux déductions contradictoires dans cette théorie? » est une question concernant plus le mathématicien logicien que l'ingénieur, même si une contradiction manifeste gênerait finalement plus le second que le premier.

Loin de nous l'idée de critiquer un tel point de vue: ce n'est pas avec de la logique méta-mathématique que l'on conçoit un pont!

Cependant il est des conceptions humaines plus récentes dont la fabrication requiert des méthodes frôlant de si près la démonstration mathématique1 que la question méta-mathématique est à son tour devenue un enjeu économique et donc, paradoxalement, pratique. Il s'agit bien entendu des conceptions informatiques. Plus généralement nous parlons des ouvrages mettant en oeuvre des procédures automatiques; l'électronique est donc par exemple aussi concernée.

Ne minimisons pas les difficultés qu'affronte le programmeur ou l'électronicien: les processeurs et logiciels actuels sont d'une complexité qu'aucun ingénieur ne risquerait sur un chantier! On peut même s'effrayer de la confiance placée dans ces programmes censés effectuer des tâches aussi critiques que piloter un train ou une fusée. Nombreux sont d'ailleurs les exemples où cette confiance s'est soldée par de coûteux ou tragiques accidents.

Comment alors s'assurer de manière rigoureuse de la correction d'un programme? De nombreux éléments de réponse ont été donnés à cette question éminemment pratique, mais l'un des plus élégants est probablement l'isomorphisme de Curry-Howard [How80], qui constate en substance qu'écrire un programme et faire une démonstration procèdent fondamentalement de la même activité. Écrire un programme correct revient donc à écrire une démonstration juste. Or c'est là la préoccupation du logicien: qu'est-ce qu'une démonstration? Comment en démontrer la justesse? Quelles théories sont cohérentes et peuvent donc servir de base à des démonstrations?

Cette préoccupation méta-mathématique s'est donc subrepticement étendue au-delà de la sphère du logicien pour pénétrer celle de l'ingénieur. Les buts de la recherche ont changé lors de ce transfert. Dans notre cas, là où il s'agissait de prouver ou de réfuter la cohérence de telle ou telle théorie, il faut maintenant démontrer que le programme de 100 000 lignes de code pilotant un métro ne provoquera pas d'accident. Un changement pour le moins radical! Devant cette constatation, les observations suivantes s'imposent:

  1. Sans outil automatique (informatique) puissant pour l'aider à concevoir ses démonstrations, l'ingénieur-logicien ne viendra pas à bout de ce travail et commettra certainement des erreurs ;
  2. La question de cohérence des théories utilisées reste entière, elle est même exacerbée par l'utilisation d'un outil automatique ;
  3. L'outil devra être lui-même vérifié préalablement pour que le travail effectué avec son aide soit réellement convaincant.
On voit ici apparaître les grandes lignes d'une branche de la recherche se situant à la frontière de la logique et de l'informatique. Elle consiste à concevoir les outils, théoriques et pratiques, qui assisteront l'utilisateur de manière rigoureuse lors des démonstrations mathématiques. L'utilisateur peut être l'ingénieur-logicien dont nous avons parlé, mais aussi l'étudiant dans le cadre de l'enseignement des mathématiques et on peut même espérer -- même s'il reste un long chemin à parcourir -- qu'à terme les mathématiciens utiliseront de tels outils pour les assister dans leur travail. Les logiciels conçus dans le cadre de cette recherche s'appellent «outil d'aide à la démonstration», «assistant de preuve»... En anglais le terme «theorem prover» semble s'imposer. Citons quelques noms de tels programmes: l'atelier B, PVS, Coq, Isabelle, NUPrl... Précisons que ces outils, bien qu'encore inadaptés à des développements de très grande taille, sont utilisés aujourd'hui dans l'industrie.

Le début de cette thèse (parties ?? et ??) s'inscrit dans l'effort actuel de conception et d'amélioration de ces outils et propose une extension du calcul des constructions inductives ( CCI ou CIC), le formalisme sous-jacent du système Coq [Coq]. Cette extension a pour but de permettre un traitement plus agréable et plus puissant de la notion de quotient, très utilisée en mathématiques. Pour comprendre ce qui se cache derrière les mots «formalisme sous-jacent», il est nécessaire d'introduire les quelques concepts fondamentaux de la logique formelle, c'est l'objet de la fin de cette introduction. Le néophyte intéressé pourra lire l'ouvrage très pédagogique de Gilles Dowek [Dow95], duquel sont tirés quelques faits historiques cités dans la suite.

La dernière partie présente le développement dans l'assistant Coq d'une preuve d'algorithme auto-stabilisant. Un algorithme auto-stabilisant est un algorithme s'exécutant sur un réseau2 et ayant la propriété suivante: à partir d'une configuration initiale quelconque du réseau, l'algorithme fait revenir celui-ci dans une configuration correcte au bout d'un temps fini et ne quitte plus les configurations correctes ensuite. On entend par configuration correcte une configuration correspondant à un déroulement valide de l'algorithme.

La méta-mathématique

L'étude du raisonnement remonte probablement plus loin, mais les philosophes grecs sont les premiers à nous en avoir laissé trace. Aristote, face à l'évidente observation qu'il existe des raisonnements faux, s'interroge sur la nature et les mécanismes de la déduction. Il constate déjà que pour déduire, il faut en premier lieu admettre des faits préalables, comme par exemple dans le raisonnement suivant: "Si on admet que tous les hommes sont mortels et que les Grecs sont des hommes, alors les Grecs sont mortels". Cette pré-admission mène à la notion de théorie.

Théorie

Le mot théorie désigne un ensemble de faits admis3, appelés axiomes. Ici les deux axiomes "tous les hommes sont mortels" et "les Grecs sont des hommes" permettent de déduire que les Grecs sont mortels.

Au risque d'enfoncer une porte ouverte, précisons qu'il n'est absolument pas correct d'en déduire que les Grecs sont mortels! On a montré qu'ils sont mortels SI on admet les deux axiomes, rien de moins, rien de plus. On reformule cet énoncé de manière plus logicienne en: «   "les Grecs sont mortels" est démontrable dans la théorie { "tous les hommes sont mortels", "les Grecs sont des hommes" }   »4. On peut également exprimer ce raisonnement lui-même sous la forme d'une propriété: "(tous les hommes sont mortels ET les Grecs sont des hommes) IMPLIQUE que les Grecs sont mortels". Cette propriété est elle-même démontrable à partir d'un ensemble d'axiomes vide: c'est une tautologie. On remarque d'ailleurs que comme dans toute tautologie, les propriétés élémentaires peuvent être remplacées par n'importe quelles autres propriétés, par exemple: "(tous les éléphants sont bleus et les poissons sont des éléphants) implique que les poissons sont bleus" est en fait la même tautologie, elle est tout aussi correcte.

Déduction

Pourtant, là encore quelque chose a été admis: la notion de raisonnement correct, autrement dit le mécanisme de déduction. En effet, sans un mécanisme pour reconnaître un raisonnement correct, comment différencier une déduction fausse d'une déduction valide? De la même manière qu'en cinétique la notion de vitesse n'a de sens qu'à l'intérieur d'un référentiel, une proposition en logique n'est donc démontrée qu'à l'intérieur d'une théorie (éventuellement vide pour les tautologies) et d'un système de déduction permettant de déduire des propriétés à partir des axiomes de la théorie. Si ce dernier est vide, alors rien n'est démontrable, pas même les axiomes. Un abus de langage autorise parfois à appeler théorie ce couple <théorie,système>.

Un système est aujourd'hui généralement présenté sous la forme d'un ensemble de règles formelles. Par exemple une règle communément admise dans tout système logique est la suivante:


  A  
(si A est un axiome)



On lit une telle règle de la manière suivante:

On voit bien ici le mécanisme de déduction défini: la règle permet de démontrer une propriété A à condition qu'elle soit un axiome. D'autres exemples classiques de règles de déduction sont le modus ponens et la règle du "et" logique:

A     A B
B
                 
A     B
A B

qui se lisent respectivement: "si A est démontrable et si A implique B (noté A B) est démontrable, alors B est démontrable", et "si A et B sont chacun démontrable, alors A et B (notée A B) est démontrable". Précisons ici que nous ne sommes pas en train d'énoncer une propriété mais bien une définition. En écrivant un ensemble de règles de déduction, on donne son sens au mot "démontrable" dans le contexte que nous avons choisi. Une démonstration se présente sous la forme d'un ensemble d'instances de règles imbriquées, formant un arbre. Par exemple, voici la preuve de a < c dans la théorie constituée des trois axiomes { a < b, b < c, (a < b b < c) a < c }:

(a < b b < c) a < c
       
a < b
       
b < c
a < b b < c
a < c

On voit que: 1) Toutes les feuilles de l'arbre contiennent des axiomes et 2) Les règles sont correctement appliquées. C'est avec ces deux critères facilement vérifiables qu'on reconnaît une déduction complète et valide. Loin d'être anodin, le besoin d'un mécanisme simple pour la vérification est au contraire primordial. En effet, si la vérification de la validité d'un raisonnement nécessite elle-même un raisonnement, alors il faut aussi s'assurer de la validité de ce dernier, ce qui demandera encore un raisonnement, etc. En fait, depuis l'apparition de la notion de machine programmable (notamment la célèbre machine théorique de Turing) et l'avènement des ordinateurs et de leur capacité à traiter des données symboliques, on a pu à la fois relâcher et préciser ce principe: il suffit que la vérification soit décidable5, c'est-à-dire qu'il soit possible d'écrire un programme (au sens programme de machine de Turing) capable de l'effectuer.

Le travail des logiciens

Le travail des logiciens consiste à définir des systèmes de déduction et des théories, et d'en étudier:

On s'est vite aperçu que plus une théorie est expressive, plus il est délicat de se convaincre puis de démontrer qu'elle est cohérente. L'exemple le plus célèbre de cette difficulté nous vient des théories des ensembles de Frege et Cantor, prouvées contradictoires par Cesare Burali-Forti puis Bertrand Russel en 1897 et 1902. Russel a pour cela exhibé la propriété suivante: "L'ensemble des ensembles qui ne se contiennent pas eux-mêmes se contient lui-même", qui est un paradoxe dans ces théories. Redéfinies par Ernst Zermelo en 1908 et par Alfred North Whithead et Russel en 1910 de manière à rendre cet énoncé impossible à formuler, ces théories n'ont finalement pas vu leur avenir remis en question et servent toujours de base aux mathématiques actuelles.

"Le" siècle de la logique

De nombreuses découvertes fondamentales, et parfois surprenantes, ont été faites dans le domaine de la logique au cours du vingtième siècle. Nous en donnons ici une petite chronologie afin de présenter brièvement les évolutions majeures de la logique récente.

1900
Gottlob Frege pose les bases de la logique formelle [Fre03]; son approche rigoureuse de la notion de preuve l'amène à définir les notions de formule et de propriété comme elles le sont encore aujourd'hui. Frege est à l'origine de la notion de système de preuve évoquée à la section précédente.

1900
La théorie naïve des ensembles est prouvée contradictoire au tout début du siècle, comme nous l'avons dit plus haut, ainsi que la théorie logique de Frege. C'est la première fois que le problème de la cohérence et sa difficulté se posent de manière si directe à l'ensemble des mathématiciens. Nous avons vu que ce problème n'a pas vraiment eu de conséquence et qu'il a été corrigé quelques années plus tard.

En fait plusieurs solutions ont été proposées, dont les suivantes:
1931
Gödel surprend la communauté mathématique en démontrant le théorème d'incomplétude [Göd31, Göd34], qui stipule que dans toute théorie permettant d'exprimer des propriétés arithmétiques (ce qui est assez minimal), il existe des propriétés qui ne sont pas démontrables et dont la négation n'est pas démontrable non plus. Par la suite, quelques problèmes ouverts bien connus sont prouvés indéterminés, c'est-à-dire appartenant à cette catégorie7 (par exemple l'hypothèse du continu est indéterminée dans la théorie des ensembles).

Ce résultat semble contrarier l'intuition mathématique: une propriété peut être soit prouvable, soit réfutable, soit ni l'un ni l'autre.

1931
Gödel ne s'arrête pas là. Puisque toute démonstration doit se faire dans une théorie, une démonstration de cohérence d'une théorie s'appuie nécessairement sur une autre théorie. Une telle démonstration est dite relative: on prouve la cohérence sous la condition que la théorie utilisée pour faire cette preuve est elle-même cohérente. Il est évident que cet exercice n'est complètement convaincant que si cette cascade s'arrête sur une théorie dont on sait qu'elle est cohérente absolument. Gödel élimine tout espoir d'un tel rêve avec son second théorème d'incomplétude: la théorie utilisée est nécessairement plus expressive que la théorie dont on cherche à prouver la cohérence. Par conséquent, on ne pourra pas arrêter la cascade.

Devant cette incapacité de la mathématique à se justifier elle-même, il ne reste plus qu'à faire acte de profession de foi, comme le fait Bourbaki à la fin de son introduction [Bou66]:
«En résumé, nous croyons que la mathématique est destinée à survivre, et qu'on ne verra jamais les parties essentielles de ce majestueux édifice s'écrouler du fait d'une contradiction soudain manifestée; mais nous ne prétendons pas que cette opinion repose sur autre chose que l'expérience. C'est peu diront certains. Mais voilà vingt-cinq siècles que les mathématiques ont l'habitude de corriger leurs erreurs et d'en voir leur science enrichie, non appauvrie; cela leur donne le droit d'envisager l'avenir avec sérénité.»
1934
Gerhard Gentzen propose le calcul des séquents [Gen69, Gen34], un système de déduction exprimant la logique du premier ordre. C'est le premier système dans lequel une propriété est démontrée non pas comme conséquence des axiomes de la théorie de base, mais comme conséquence d'un ensemble de propriétés construit au cours de la déduction. Les règles, toujours sous la forme de fractions comme plus haut, sont constituées de séquents au lieu de formules (propriétés). Un séquent G |- A signifie "A est démontrable sous l'ensemble d'hypothèses G". Par exemple, la règle de déduction du et logique s'exprime de la manière suivante:
G |- A G |- B
G |- A B
On lit cette règle de la manière suivante: On voit que ce système met l'accent sur la notion de conséquence plus que sur celle de vérité. Il permet notamment d'ajouter des hypothèses au cours du raisonnement. Il est clair aujourd'hui que cette vision est plus souple et plus conforme au raisonnement intuitif. Un autre avantage de cette approche est qu'il n'y a plus d'axiome à proprement parler, seulement une règle permettant de déduire une propriété A d'un ensemble d'hypothèses contenant A:
A Î G
G |- A

1936
L'opinion de Hilbert, selon laquelle les mécanismes de raisonnement décrits dans les systèmes logiques ne sont que des méthodes de calcul pouvant être automatisées, est réfutée à la fois par Church et Turing. Ils montrent qu'il existe des problèmes qui ne sont pas décidables, c'est-à-dire qu'aucun calcul n'est capable de les résoudre. C'est en particulier le cas du problème consistant à prendre une propriété quelconque P et de répondre à la question «P est-elle démontrable dans la théorie des ensembles8?».

Cette découverte décevante nous intéresse particulièrement car elle signifie que le projet d'un programme de démonstrations mathématiques complètement automatique est voué à l'échec.

1930-40
Parallèlement, Alonzo Church développe le l-calcul [Chu40], un formalisme permettant d'exprimer les fonctions sous la forme d'algorithmes (de termes), accompagné d'une notion de calcul permettant d'évaluer les fonctions lorsqu'elles sont appliquées à leurs arguments. Par exemple, la fonction identité est représentée de la manière suivante:
l x.x
qui se lit «fonction qui prend un argument auquel on donnera le nom x à l'intérieur de la définition9, et qui rend x».

On peut appliquer cette fonction à un terme t:
(l x.x t)
et le mécanisme de calcul stipule qu'il faut alors faire disparaître l'abstraction et remplacer l'argument abstrait par l'argument réel, ce qui redonne t dans notre cas:
(l x.x t) t

De même le terme l z.z+1 est intuitivement la fonction qui rend la valeur de son argument (appelé z à l'intérieur de la définition) incrémentée de un. Il faut ici préciser que 1 et + ne font pas partie du l-calcul et doivent être codés de manière assez subtile sous forme de termes. Nous reviendrons sur cet aspect peu pratique pour justifier les dernières évolutions de la théorie des types à la fin de cette section. Nous étudions plus en détail le l-calcul et ses versions typées dans la partie ?? de cette thèse.

Cette représentation intentionnelle des fonctions intéresse Church d'une part pour étudier les fonctions et leur comportement calculatoire (cet aspect a donné naissance aux langages de programmation fonctionnels) et d'autre part pour lui adjoindre des règles logiques afin de définir un nouveau système de déduction, appelé "logique d'ordre supérieur" et capable de remplacer la théorie des ensembles10. L'idée principale est d'utiliser comme brique de base non plus l'ensemble -- comme en théorie des ensembles -- mais la fonction. Plus explicitement: de même que la définition des entiers (et de tout autre concept) en théorie des ensembles passe par un codage utilisant des ensembles, de même en théorie des types les entiers (dits de Church) sont codés par des fonctions.

La première version de ce système s'avère contradictoire mais les suivantes, grâce à la notion de type associé à un terme, sont prouvées cohérentes (relativement à la théorie des ensembles). Le l-calcul et ses avatars servent aujourd'hui de fondement à de nombreux systèmes de preuves actuels, où il est fait un usage intensif de la possibilité de représenter des fonctions intentionnellement (c'est-à-dire en donnant un algorithme pour les calculer). Cet aspect est d'ailleurs souvent présenté comme l'avantage majeur de la théorie des types sur la théorie des ensembles comme fondement des assistants de preuve.

1965
Dag Prawitz propose le système de Déduction naturelle [Pra65] (voir également section ?? figure ??), du même genre que celui de Gentzen. On s'aperçoit alors que les règles de ce système sont les mêmes que les règles de typage du l-calcul. Cet isomorphisme, dit de Curry-Howard, fait apparaître que les preuves faites dans ce système sont isomorphes aux l-termes. De ce fait, un l-terme est à la fois un objet mathématique (une fonction de A dans B, un entier...) et une preuve (la preuve que A B, la preuve que l'ensemble des entiers contient un élément...). De même les types correspondent aux propositions et une proposition (un type) est donc prouvable s'il existe un terme ayant pour type cette proposition. C'est l'idée principale de la théorie des types de Martin-Löf (ci-dessous). Les conséquences de cet isomorphisme sont étonnamment riches et continuent d'être découvertes de nos jours. C'est la pierre angulaire des démonstrateurs tels que Coq ou Lego, qui utilisent les l-termes pour représenter les preuves et le typage de ces termes pour vérifier de quoi ils sont la preuve.

1969
Per Martin-Löf décrit la théorie des types intuitionniste [ML84], un système de déduction pour les mathématiques constructives (c'est-à-dire intuitionnistes). Son originalité réside dans l'utilisation de l'isomorphisme de Curry-Howard pour interpréter la notion de démonstration à l'intérieur même du formalisme. Une proposition est interprétée comme un ensemble, dont les éléments représentent les preuves possibles de cette proposition. Une proposition indémontrable est donc représentée par l'ensemble vide et une proposition démontrable par un ensemble non vide.



Remarque: Les systèmes logiques issus de la théorie des types sont en général présentés sous la forme d'un système de typage du type l-calcul grâce à l'isomorphisme de Curry-Howard. Nous adopterons aussi cette présentation tout au long de cette thèse.

1970 à nos jours
De nombreux systèmes ont été proposés depuis; un des critères intéressants pour ces systèmes est la réduction des étapes de codage nécessaires pour définir les concepts. On a vu en effet que dans le l-calcul et la théorie des types, la définition de notions aussi simples que N passait par des codages lourds et peu adaptés à une implantation sur machine. En plus des critères de cohérence et d'expressivité, le souci grandissant d'une implantation a donc poussé les logiciens vers de nouveaux formalismes plus riches et plus souples que les anciens systèmes jusque là très minimaux. Nous en donnons ici une très courte liste. À chaque nouveau système, des commodités supplémentaires sont introduites dans le formalisme, compliquant son analyse mais facilitant sa mise en oeuvre informatique et la création des outils de démonstration.

Le but de cette thèse est

Plan de la thèse

La partie ?? est consacrée à la présentation progressive de différents l-calculs: les l-calculs pur et typé, puis le calcul des constructions et enfin le calcul des constructions inductives. On introduira également quelques notions importantes comme l'isomorphisme de Curry-Howard, la sémantique de Heyting (section ??). Le lecteur familier de ces concepts pourra éviter de lire les premiers chapitres. Le dernier chapitre est une courte présentation de l'assistant de preuve Coq, dans lequel on illustre certains principes expliqués jusque là.

La partie ?? présente le calcul des constructions inductives avec types normalisés ainsi que les preuves de ses différentes propriétés.

Enfin la dernière partie décrit un développement en Coq d'une preuve d'algorithme auto-stabilisant. On y trouvera notamment quelques définitions et résultats concernant la réécriture sur les mots.


1
Nous verrons plus loin que ces méthodes consistent exactement en des démonstrations mathématiques.
2
Un tel algorithme est dit réparti.
3
Le mot théorie désigne aussi parfois l'ensemble des théorèmes démontrables à partir des axiomes.
4
L'ensemble des propriétés démontrables dans une théorie est l'ensemble des propriétés qu'on peut déduire des axiomes. On verra qu'une déduction se fait à l'aide d'un système de règles de déduction, lui-même défini au préalable.
5
Cette notion, la décidabilité, est définie de manière très précise et caractérise tous les problèmes que le calcul sans raisonnement est capable de résoudre. Il est très courant de définir par inadvertance une notion de vérification indécidable, c'est-à-dire qu'aucun programme ne pourra effectuer dans tous les cas.
6
Ce n'est pas la théorie des types dont il est question dans cette thèse; nous y parlerons de la théorie des types de Martin-Löf, laquelle est en effet une reformulation intuitionniste de celle de Russel.
7
On dit aussi qu'une propriété est indépendante d'une théorie.
8
Ainsi que dans toute autre théorie ayant une expressivité comparable, l'indécidabilité réside bien dans la logique exprimée par le système et non dans sa formulation.
9
x est donc un argument abstrait, c'est la signification de la notation l x.
10
Ce but ne sera pas atteint de la manière imaginée par Church car le l-calcul typé n'est pas assez expressif. C'est la théorie des types de Martin-Löf qui y parviendra, voir plus bas.

References

[Bou66]
N. Bourbaki. Théorie des ensembles. In Éléments de mathématiques. Hermann, 1966.

[CH88]
Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95--120, February 1988.

[Chu40]
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.

[Coq]
The Coq Proof Assistant. http://coq.inria.fr/.

[CPM90]
Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

[Dow95]
G. Dowek. La logique. Flammarion, 1995.

[Fre03]
G. Frege. Grundgesetze der Arithmetik, Begriffsschriftlich abgeleitet. Verlag Hermann Pohle, Jena, 1893--1903.

[Gen34]
G. Gentzen. Untersuchungen über das logische schliessen, 1934.

[Gen69]
G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen. North-Holland, 1969.

[GLT89]
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Göd31]
K. Gödel. Uber formal unentscheidbare satze der principia mathematica und verwandter systeme, 1931.

[Göd34]
K. Gödel. On undecidable propositions of formal mathematical systems; in: Collected works, 1934.

[Hey56]
A. Heyting. Intuitionism: An Introduction. North-Holland, Amsterdam, 1956.

[How80]
William A. Howard. The formulae-as-types notion of construction. In J. Roger Hindley Jonathan P. Seldin, editor, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, London, 1980.

[ML84]
Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984.

[PM93]
Christine Paulin-Mohring. Inductive definitions in the system COQ. In Typed Lambda Calculi and Applications, pages 328--345. Springer-Verlag, 1993. LNCS 664.

[PM96]
Christine Paulin-Mohring. Définitions inductives en théorie des types d'ordre supérieur. thèse d'habilitation, Décembre 1996.

[Pra65]
Dag Prawitz. Natural Deduction, A Proof-Theoretical Study. Almqvist & Wiksell, 1965.

[Wer94]
Benjamin Werner. Méta-théorie du Calcul des Constructions Inductives. Thèse de doctorat, Univ. Paris VII, 1994.

This document was translated from LATEX by HEVEA.
Pierre Courtieu
Last modified: Tue Oct 1 18:19:56 MEST 2002