Bibliographie

[a] G. Dowek, Lambda-calculus, combinators and the comprehension scheme, M. Dezani-Ciancaglini and G. Plotkin (Eds.), *Typed lambda calculi and applications*, Lecture notes in computer science 902, Springer-Verlag (1995), pp. 154-170. *Rapport de Recherche* 2565, INRIA (1995).

[b] G. Dowek, *Collections, sets and types*, *Mathematical structures in computer science*, 9 (1999), pp. 1-15.

[c] G. Dowek, Th. Hardin, and C. Kirchner, Higher-order unification via explicit substitutions, *Logic in computer science* (1995), pp. 366-374. *Information and Computation* (to appear).

[d] G. Dowek, Th. Hardin, C. Kirchner, and F. Pfenning, Higher-order unification via explicit substitutions : the case of higher-order patterns, M. Maher (Ed.), *Joint International Conference and Symposium on Logic Programming* (1996), pp. 259-273. *Rapport de Recherche* 3591, INRIA (1998).

[e] G. Dowek, Proof normalization for a first-order formulation of higher-order logic, E.L. Gunter and A. Felty (Eds.), *Theorem Proving in Higher-order Logics*, Lecture notes in computer science 1275, Springer-Verlag (1997), pp. 105-119. *Rapport de Recherche* 3383, INRIA (1998).

[f] G. Dowek, A Type-free formalization of mathematics where proofs are objects, E. Giménez and Ch. Paulin-Mohring (Eds.), *Types for proofs and programs*, Lecture notes in computer science 1512, Springer-Verlag (1998), pp. 88-111. *Rapport de Recherche* 2915, INRIA (1996).

[g] G. Dowek, Th. Hardin, and C. Kirchner, Theorem proving modulo, *Rapport de Recherche* 3400, INRIA (1998).

[h] G. Dowek and B. Werner, Proof normalization modulo, *Types for proofs and programs* (1998) (to appear). *Rapport de Recherche* 3542, INRIA (1998).

[i] G. Dowek, Th. Hardin, and C. Kirchner, HOL-λσ : an intentional first-order expression of higher-order logic, *Rewriting Techniques and Applications* (1999) (to appear). *Rapport de Recherche* 3556, INRIA (1998).

[j] G. Dowek, Automated theorem proving in first-order logic modulo : on the difference between type theory and set theory. *First-order theorem proving* (1998) (to appear).

[x] G. Dowek, *Le sens du calcul*, manuscript.

[y] G. Dowek, *Le langage mathématique et les langages de programmation*, manuscript.

[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy, Explicit substitutions, *Journal of Functional Programming*, 4, 1 (1991), pp. 375-416.

[2] T. Altenkirch, Constructions, inductive types and strong normalization, Ph.D., University of Edinburgh (1993).

[3] P.B. Andrews, Resolution in type theory, *The Journal of Symbolic Logic*, 36 (1971), pp. 414-432.

[4] P.B. Andrews, General models, descriptions and choice in type theory, *The Journal of Symbolic Logic*, 37, 2 (1972), pp. 385-394.

[5] P.B. Andrews, General models and extensionality, *The Journal of Symbolic Logic*, 37, 2 (1972), pp. 395-397.
[6] P.B. Andrews, An introduction to mathematical logic and type theory : to truth through proof, *Aca-demic Press* (1986).

[7] P.B. Andrews, D.A. Miller, E. Longini Cohen, and F. Pfenning, Automating higher-order logic, W.W. Bledsoe and D.W. Loveland (Eds.), *Automated theorem proving : after 25 years*, Contemporary Mathematics Series 29, American Mathematical Society (1984), pp. 169-192.

[8] S.C. Bailin, A normalization theorem for set theory, *The Journal of Symbolic Logic*, 53, 3 (1988), pp. 673-695.

[9] S.C. Bailin, A λ-unifiability test for set theory, *Journal of Automated Reasoning*, 4 (1988), pp. 269-286.

[10] H.P. Barendregt, The lambda-calculus, its syntax and semantics, second edition, *North-Holland* (1984).

[11] H.P. Barendregt, Lambda calculi with types, S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum (Eds.), *Handbook of Logic in Computer Science*, Vol. 2, Clarendon Press (1992), pp. 118-309.

[12] H. Barendregt and E. Barendsen, Autarkic computations in formal proofs, manuscript.

[13] P. Borovanský, Implementation of higher-order unification based on calculus of explicit substitution, M. Bartošek, J. Staudek, and J. Wiedermann (Eds.) *SOFSEM'95 : Theory and Practice of Informatics*, Lecture notes in computer science 1012, Springer-Verlag (1995), pp. 363-368.

[14] R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert and J. Van Tassel, Experience with embedding hardware description languages in HOL, V. Stavridou, T.F. Melham and R. T. Boute (Eds.), *IFIP TC10/WG 10.2, International Conference on Theorem Provers in Circuit Design : Theory, Practice and Experience*, IFIP Transactions volume A-10, North-Holland/Elsevier (1992), pp. 129-156.

[15] Th. Coquand and G. Huet, The calculus of constructions, *Information and Computation*, 76 (1988), pp. 95-120.

[16] A. Church, A formulation of the simple theory of types, *The Journal of Symbolic Logic*, 5 (1940), pp. 56-68.

[17] A. Church, The calculi of lambda-conversion (1941).

[18] A. Church, Introduction to mathematical logic, *Princeton University Press* (1956).

[19] P.-L. Curien, Categorical combinators, sequential algorithms and functional programming, second edition, *Birkhäuser* (1993).

[20] P.-L. Curien and A. Rios, Un résultat de compléture pour les substitutions explicites, *Compte-rendus à l'Académie des Sciences de Paris*, I, 312 (1991), pp. 471-476.

[21] P.-L. Curien, Th. Hardin, and J.-J. Lévy, Confluence properties of weak and strong calculi of explicit substitutions, *Journal of the Association for Computing Machinery*, 43, 2 (1996), pp. 362-397.

[22] H.B. Curry, The combinatory foundations of mathematical logic, *The Journal of Symbolic Logic*, 7, 2 (1942), pp. 49-64.

[23] H.B. Curry and R. Feys, Combinatory logic, Vol. 1, *North-Holland* (1958).

[24] M. Davis, Invited commentary to [85], *International Federation for Information Processing Congress*, North-Holland (1968), pp. 67-68.

[25] N.G. De Bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula ma-nipulation, with application to the Church-Rosser theorem, *Indagationes Mathematicae*, 5, 34 (1972), pp. 381-392.

[26] N.G. De Bruijn, A Survey of the project Automath, To H.B. Curry : essays on combinatory logic, lambda calculus and formalism, Academic Press (1980) pp. 579-606.

[27] D.J. Dougherty, Higher-order unification via combinators, *Theoretical Computer Science*, 114 (1993), pp. 273-298.

[28] J. Ekman, Normal proofs in set theory, *Doctoral thesis*, Chalmers University of Technology and University of Göteborg (1994).
[29] H.B. Enderton, A mathematical introduction to logic, *Academic Press* (1972).

[30] M. Fay, First-order unification in an equational theory, *Fourth Workshop on Automated Deduction* (1979), pp. 161-167.

[31] S. Feferman, Finitary inductively presented logics, *Logic Colloquium*, R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo (Eds.), *North-Holland* (1989).

[32] S. Feferman, Reflecting on incompleteness, *The Journal of Symbolic Logic*, 56, 1, (1991), pp. 1-49.

[33] J. Gallier, Logic in computer science, *Harper and Row* (1986).

[34] J. Gallier, On Girard's *candidats de réductibilité*, P. Odifreddi (Ed.), *Logic and Computer Science*, Academic Press (1990), pp. 123-203.

[35] J. Gallier and W. Snyder, Complete set of transformations for general E-unification, *Theoretical Computer Science*, 67, 2-3 (1989), pp. 203-260.

[36] J.-Y. Girard, Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types, J.E. Fenstad (Ed.), *Second Scandinavian Logic Symposium*, North-Holland (1970).

[37] J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, *Thèse d'État*, Université de Paris VII (1972).

[38] J.-Y. Girard, Y. Lafont, and P. Taylor, Proofs and types, *Cambridge University Press* (1989).

[39] P. Gochet et P. Gribomont, Logique, *Hermès* (1990, 1994).

[40] H. Goguen and J. Goubault-Larrecq, Sequent combinators : a Hilbert system for the lambda calculus, manuscript.

[41] J. Goubault-Larrecq, A proof of weak termination of the simply typed $\lambda\sigma$-calculus, *Rapport de Recherche* 3090, INRIA (1997).

[42] L. Hallnäs, On normalization of proofs in set theory, *Doctoral thesis*, University of Stockholm (1983).

[43] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. *Journal of the Association for Computing Machinery*, 40, 1 (1993), pp. 143-184.

[44] Th. Hardin, L. Maranget, and B. Pagano, Functional back-ends within the lambda-sigma calculus, *Journal of Functional Programming*, 8, 2 (1998), pp. 131-176.

[45] L. Henkin, Completeness in the theory of types, *The Journal of Symbolic Logic*, 15 (1950), pp. 81-91.

[46] L. Henkin, Banishing the rule of substitution for functional variables, *The Journal of Symbolic Logic*, 18, 3 (1953), pp. 201-208.

[47] J.R. Hindley, Combinatory reductions and lambda reductions compared, *Zeitschrift für Mathematische Logik und Grundlagen der Mathematik*, 23 (1977), pp. 169-180.

[48] J.R. Hindley and J.P. Seldin, Introduction to combinators and $\lambda$-calculus, *Cambridge University Press* (1986).

[49] W.A. Howard, The Formulæ-as-type notion of construction, 1969, J.R. Hindley and J.P. Seldin (Eds.), *To H.B. Curry : essays on combinatory logic, lambda calculus and formalism*, Academic Press (1980) pp. 479-490.

[50] G. Huet, Constrained resolution : a complete method for higher order logic, *Ph.D.*, Case Western Reserve University (1972).

[51] G. Huet, A mechanization of type theory, *International Joint Conference on Artificial Intelligence* (1973), pp. 139-146.

[52] G. Huet, A unification algorithm for typed lambda calculus, *Theoretical Computer Science*, 1, 1 (1975), pp. 27-57.

[53] G. Huet, Résolution d'équations dans les Langages d'Ordre 1,2, ..., $\omega$, *Thèse d'État*, Université de Paris VII (1976).
[54] R.J.M. Hughes, Super-combinators, a new implementation method for applicative languages, *Lisp and Functional Programming* (1982), pp. 1-20.

[55] J.-M. Hullot, Canonical forms and unification, W. Bibel and R. Kowalski (Eds.) *Conference on Automated Deduction*, Lecture notes in computer science 87, Springer-Verlag (1980), pp. 318-334.

[56] J. Hsiang, Refutational theorem proving using term-rewriting systems, *Artificial Intelligence*, 25 (1985), pp. 255-300.

[57] J.-P. Jouannaud and C. Kirchner, Solving equations in abstract algebras : a rule-based survey of unification, J.-L. Lassez and G. Plotkin (Eds.) *Computational logic. Essays in honor of Alan Robinson*, MIT press (1991), pp. 257-321.

[58] J.W. Klop, V. van Oostrom, and F. van Raamsdonk, Combinatory reduction systems : introduction and survey, *Theoretical Computer Science*, 121 (1993), pp. 279-308.

[59] J.-L. Krivine, Lambda-calcul, types et modèles, *Masson* (1990).

[60] J.L. Krivine and M. Parigot, Programming with proofs, *J. Inf. Process. Cybern. EIK* 26 (1990), pp. 149-167.

[61] A. Lalande, entrée *lexis*, Vocabulaire technique et critique de la philosophie, *Presses Universitaires de France* (1951).

[62] L. Magnusson, The implementation of ALF, a proof editor based on Martin-Löf monomorphic type theory with explicit substitution, *Doctoral thesis*, Chalmers University of Technology and University of Göteborg (1994).

[63] L. Maranget, Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems, *Principle of Programming Languages* (1991), pp. 255-269.

[64] P. Martin-Löf, Constructive mathematics and computer programming, *Logic, Methodology and Philosophy of Science*, L.J. Cohen, J. Łoś, H. Pfeiffer, and K.-P. Podewski (Eds.), North-Holland (1982), pp. 153-175.

[65] P. Martin-Löf, Intuitionistic type theory, *Bibliopolis* (1984).

[66] P. Martin-Löf, Personal communication.

[67] V. McGee, How truthlike can a predicate be? A negative result, *Journal of Philosophical Logic*, 14 (1985), pp. 399-410.

[68] P.-A. Melliès, Typed λ-calculi with explicit substitutions may not terminate, M. Dezani-Ciancaglini and G. Plotkin (Eds.), *Typed Lambda Calculi and Applications* (1995).

[69] E. Mendelson, Introduction to mathematical logic, *Van Nostrand* (1963).

[70] D.A. Miller, Proofs in higher order logic, Ph.D., Carnegie Mellon University (1983).

[71] D.A. Miller, A compact representation of proofs, *Studia Logica*, 46, 4 (1987), pp. 347-370.

[72] D.A. Miller, Unification under a mixed prefix, *Journal of Symbolic Computation*, 4, 14 (1992), pp. 321-358.

[73] D.A. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, *Journal of Logic and Computation*, 1, 4 (1991), pp. 497-536.

[74] C.A. Muñoz-Hurtado, Un calcul de substitutions pour la représentation des preuves partielles en théorie des types, *Thèse de Doctorat*, Université de Paris VII (1997).

[75] C.A. Muñoz-Hurtado, A calculus of substitutions for incomplete-proof representation in type theory, *Rapport de Recherche* 3309, INRIA (1997).

[76] C.A. Muñoz-Hurtado, A left-linear variant of λσ, *International Conference PLILP/ALP/HOA* 1997, Lecture notes in computer science 1298, Springer-Verlag (1997) pp. 224-239.

[77] C.A. Muñoz-Hurtado, Dependent types with explicit substitutions : a meta-theoretical development, E. Giménez and Ch. Paulin-Mohring (Eds.), *Types for proofs and programs*, Lecture notes in computer science 1512, Springer-Verlag (1998), pp. 294-316.
[78] Ch. Paulin-Mohring, Inductive definitions in the system COQ, Rules and properties, *Typed Lambda Calculi and Applications*, Lecture notes in computer science 664, Springer-Verlag (1993), pp. 328-345.

[79] Ch. Paulin-Mohring and B. Werner, Synthesis of ML programs in the system Coq. *Journal of Symbolic Computation*, 15 (1993), pp. 607-640.

[80] G. Plotkin, Building-in equational theories, *Machine Intelligence*, 7 (1972), pp. 73-90.

[81] H. Poincaré, La science et l'hypothèse, 1902, Flammarion (1968).

[82] W.V.O. Quine, Set theory and its logic, *Belknap press* (1969).

[83] A. Ríos, Contributions à l'étude des λ-calculs avec des substitutions explicites, *Thèse de Doctorat*, Université de Paris VII (1993),

[84] J. A. Robinson, A Machine-oriented logic based on the resolution principle, *Journal of the Association for Computing Machinery*, 12, 1 (1965), pp. 23-41.

[85] J.A. Robinson, New directions in mechanical theorem proving, *International Federation for Information Processing Congress, North-Holland* (1968), pp. 63-67.

[86] W. Snyder and J. Gallier, Higher-order unification revisited : complete sets of transformations, *Journal of Symbolic Computation*, 8 (1989), pp. 101-140.

[87] M. Stickel, Automated deduction by theory resolution, *Journal of Automated Reasoning*, 4, 1 (1985), pp. 285-289.

[88] T. Strahm, Partial applicative theories and explicit substitutions, *Journal of Logic and Computation* 6, 1 (1996), pp. 55-77.

[89] W.W. Tait, Intensional interpretation of functionals of finite type I, *The Journal of Symbolic Logic*, 32, 2 (1967), pp. 198-212.

[90] A. Werner, Normalizing narrowing for weakly terminating and confluent systems, U. Montanari and F. Rossi, (Eds.), *First International Conference on Principles and Practice of Constraint Programming*, Lecture notes in computer science 976, Springer-Verlag (1995), pp. 415-430.

[91] B. Werner, Une théorie des constructions inductives, *Thèse de Doctorat*, Université de Paris VII (1994).

[92] A.N. Whitehead and B. Russell, Principia mathematica, *Cambridge University Press* (1910-1913, 1925-1927).
# Table des matières

<table><tbody><tr><td>1</td><td>La déduction modulo</td><td>11</td></tr><tr><td>1.1</td><td>Les règles</td><td>11</td></tr><tr><td>1.2</td><td>Les congruences</td><td>14</td></tr><tr><td>1.2.1</td><td>La réécriture des termes</td><td>14</td></tr><tr><td>1.2.2</td><td>Les équations entre termes</td><td>14</td></tr><tr><td>1.2.3</td><td>La réécriture des propositions</td><td>14</td></tr><tr><td>1.3</td><td>Le lemme d'équivalence</td><td>15</td></tr><tr><td>1.4</td><td>La notion de modèle pour la déduction modulo</td><td>15</td></tr><tr><td>1.5</td><td>Le cas des congruences présentées par un système de réécriture</td><td>16</td></tr><tr><td>2</td><td>La théorie des types simples</td><td>19</td></tr><tr><td>2.1</td><td>La théorie naïve des ensembles</td><td>19</td></tr><tr><td>2.2</td><td>La théorie des types simples</td><td>20</td></tr><tr><td>2.3</td><td>Le symbole ε</td><td>22</td></tr><tr><td>2.3.1</td><td>Les contenus propositionnels</td><td>22</td></tr><tr><td>2.3.2</td><td>Les termes, les propositions et les assertions</td><td>23</td></tr><tr><td>2.4</td><td>Le langage des termes et l'intentionnalité</td><td>24</td></tr><tr><td>2.4.1</td><td>La substitution des variables de fonction et de prédicat</td><td>24</td></tr><tr><td>2.4.2</td><td>Le schéma de compréhension</td><td>24</td></tr><tr><td>2.4.3</td><td>Les combinateurs</td><td>24</td></tr><tr><td>2.4.4</td><td>Le λ-calcul</td><td>26</td></tr><tr><td>2.4.5</td><td>Le calcul des substitutions explicites</td><td>27</td></tr><tr><td>2.4.6</td><td>Les combinateurs, à nouveau</td><td>31</td></tr><tr><td>2.4.7</td><td>Le calcul faible des substitutions explicites</td><td>34</td></tr><tr><td>2.4.8</td><td>En conclusion : quel langage?</td><td>35</td></tr><tr><td>2.5</td><td>La complétude</td><td>35</td></tr><tr><td>2.6</td><td>La skolémisation</td><td>35</td></tr><tr><td>2.6.1</td><td>Le problème de la skolémisation en théorie des types</td><td>35</td></tr><tr><td>2.6.2</td><td>La skolémisation dans la présentation de la théorie des types utilisant les combinateurs</td><td>37</td></tr><tr><td>2.6.3</td><td>La skolémisation dans la présentation de la théorie des types utilisant des substitutions explicites</td><td>37</td></tr><tr><td>3</td><td>La théorie des ensembles</td><td>39</td></tr><tr><td>3.1</td><td>La théorie des ensembles de Zermelo</td><td>39</td></tr><tr><td>3.2</td><td>Le langage des termes</td><td>40</td></tr></tbody></table>
<table>
  <tbody>
    <tr>
      <td>4</td>
      <td>L'élimination des coupures</td>
      <td>43</td>
    </tr>
    <tr>
      <td>4.1</td>
      <td>Les coupures en déduction modulo</td>
      <td>43</td>
    </tr>
    <tr>
      <td>4.2</td>
      <td>La notation fonctionnelle des démonstrations</td>
      <td>44</td>
    </tr>
    <tr>
      <td>4.3</td>
      <td>La réductibilité</td>
      <td>46</td>
    </tr>
    <tr>
      <td>4.3.1</td>
      <td>L'élimination des coupures en logique du premier ordre</td>
      <td>46</td>
    </tr>
    <tr>
      <td>4.3.2</td>
      <td>L'élimination des coupures en déduction modulo</td>
      <td>47</td>
    </tr>
    <tr>
      <td>4.3.3</td>
      <td>Les prémodèles</td>
      <td>47</td>
    </tr>
    <tr>
      <td>4.3.4</td>
      <td>La conjecture de normalisation</td>
      <td>49</td>
    </tr>
    <tr>
      <td>4.3.5</td>
      <td>Des prémodèles aux modèles</td>
      <td>49</td>
    </tr>
    <tr>
      <td>4.4</td>
      <td>Les coupures de conversion</td>
      <td>50</td>
    </tr>
    <tr>
      <td>4.5</td>
      <td>La normalisation des démonstrations du théorème de Cantor</td>
      <td>50</td>
    </tr>
    <tr>
      <td>4.5.1</td>
      <td>En théorie des types avec une fonction</td>
      <td>50</td>
    </tr>
    <tr>
      <td>4.5.2</td>
      <td>En théorie des types avec une relation</td>
      <td>51</td>
    </tr>
    <tr>
      <td>4.5.3</td>
      <td>En théorie des ensembles</td>
      <td>52</td>
    </tr>
    <tr>
      <td>4.5.4</td>
      <td>Dans les théories étendues</td>
      <td>53</td>
    </tr>
    <tr>
      <td>4.6</td>
      <td>Les démonstrations objets de la théorie</td>
      <td>54</td>
    </tr>
    <tr>
      <td>4.6.1</td>
      <td>Les motivations</td>
      <td>54</td>
    </tr>
    <tr>
      <td>4.6.2</td>
      <td>Le plongement des théories du premier ordre dans le λ-calcul</td>
      <td>54</td>
    </tr>
    <tr>
      <td>4.6.3</td>
      <td>Le plongement des théories modulo dans le λ-calcul</td>
      <td>55</td>
    </tr>
    <tr>
      <td>4.6.4</td>
      <td>Le cas de la théorie des types simples</td>
      <td>55</td>
    </tr>
    <tr>
      <td>5</td>
      <td>La démonstration automatique</td>
      <td>59</td>
    </tr>
    <tr>
      <td>5.1</td>
      <td>La résolution équationnelle</td>
      <td>59</td>
    </tr>
    <tr>
      <td>5.2</td>
      <td>La résolution modulo</td>
      <td>60</td>
    </tr>
    <tr>
      <td>5.2.1</td>
      <td>La règle de surréduction étendue</td>
      <td>60</td>
    </tr>
    <tr>
      <td>5.2.2</td>
      <td>Les contraintes</td>
      <td>61</td>
    </tr>
    <tr>
      <td>5.2.3</td>
      <td>La complétude</td>
      <td>61</td>
    </tr>
    <tr>
      <td>5.2.4</td>
      <td>Un exemple simple</td>
      <td>61</td>
    </tr>
    <tr>
      <td>5.3</td>
      <td>La démonstration automatique en théorie des types simples</td>
      <td>63</td>
    </tr>
    <tr>
      <td>5.3.1</td>
      <td>La surréduction et la scission</td>
      <td>63</td>
    </tr>
    <tr>
      <td>5.3.2</td>
      <td>L'unification équationnelle et l'unification d'ordre supérieur</td>
      <td>64</td>
    </tr>
    <tr>
      <td>5.3.3</td>
      <td>De la résolution d'ordre supérieur à la résolution modulo</td>
      <td>65</td>
    </tr>
    <tr>
      <td>5.4</td>
      <td>La démonstration automatique en théorie des ensembles</td>
      <td>65</td>
    </tr>
    <tr>
      <td>6</td>
      <td>Les types et la terminaison</td>
      <td>67</td>
    </tr>
    <tr>
      <td>6.1</td>
      <td>Les types et les ensembles</td>
      <td>67</td>
    </tr>
    <tr>
      <td>6.2</td>
      <td>La réduction dans un cadre monosorté</td>
      <td>68</td>
    </tr>
    <tr>
      <td>6.3</td>
      <td>Les démonstrations objets de la théorie</td>
      <td>69</td>
    </tr>
    <tr>
      <td>6.3.1</td>
      <td>Les motivations</td>
      <td>69</td>
    </tr>
    <tr>
      <td>6.3.2</td>
      <td>Une formulation sans types des mathématiques où les démonstrations sont des objets</td>
      <td>69</td>
    </tr>
    <tr>
      <td>6.3.3</td>
      <td>Le paradoxe de Tarski</td>
      <td>70</td>
    </tr>
    <tr>
      <td>6.3.4</td>
      <td>Le problème de la cohérence</td>
      <td>71</td>
    </tr>
    <tr>
      <td>6.4</td>
      <td>Une restriction de la théorie des ensembles</td>
      <td>71</td>
    </tr>
  </tbody>
</table>
# Index

ascension des variables (λ-lifting), 26

axiome
de conversion, 21, 25
de Curry, 27

β-réduction, 26

calcul, 7
des séquents, 11
candidat de réductibilité, 46
combinateur, 24
catégorique, 27

congruence, 11
conjecture de normalisation, 49

contenu propositionnel, 20
contrainte, 61

coupure, 43
de conversion, 50

cube de Barendregt, 57

décidabilité de la congruence, 14

déduction
modulo, 11
naturelle, 11

démonstration automatique, 8, 59

élimination des coupures, 8, 43
ε, 20

équation, 14

η-réduction, 31

fonction partielle, 69
Fondations nouvelles (New foundations), 68

imprédicativité, 71
indice
de De Bruijn, 27
de Skolem, 36

isomorphisme de Curry-De Bruijn-Howard, 44, 69

λ-calcul, 26
avec des constructeurs de types, 49, 57
avec des substitutions explicites, 27

avec des types dépendants, 54
avec des types dépendants modulo, 54
avec des types inductifs, 57
faible avec des substitutions explicites, 34
polymorphe, 49, 57

λσ-calcul, 27
lemme
d'équivalence, 15
de conservativité, 16

lexis, 23

méthode de Tait, 46
modèle, 15, 49

opérateur de descriptions, 54, 69

paradoxe
de Russell, 19
de Tarski, 23, 70

plongement
d'une théorie dans le λ-calcul, 54
d'une théorie modulo dans le λ-calcul, 55

précuisson (pre-cooking), 30, 64

prémodèle, 48

programmation en langage mathématique, 8, 54

proposition de Crabbé, 40, 44, 65

raisonnement, 7
réductible, 46
règle
de réduction des démonstrations, 44
de réécriture, 14

de la théorie des ensembles, 40
de la théorie des types simples, 22
de typage des démonstrations, 45

résolution
équationnelle, 59
modulo, 60

schéma de compréhension, 19, 24
fermé, 25
ouvert, 25

scission, 60
sémantique de Brouwer-Heyting-Kolmogorov, 44, 69

skolémisation

de la théorie des ensembles, 39

de la théorie des types, 21

de la théorie naïve des ensembles, 19

en théorie des types, 35

stratifiable, 49, 68, 72

substitution

des indices de De Bruijn, 28

des variables de fonction et de prédicat, 24

du λ-calcul, 26

surréduction, 59

étendue, 60

système de réduction combinatoire (*combinatory reduction systems*), 15

théorème

d'incomplétude (second), 49

de Cantor, 50

de complétude, 16, 35

de complétude de la résolution modulo, 61

de correction, 16

de l'effondrement, 35

de Tait, 22

théorie

des ensembles, 39

des ensembles de Von Neumann-Bernays-Gödel, 40

des types simples, 20

naïve des ensembles, 19

unification

d'ordre supérieur, 64

équationnelle, 59

valeur, 9

vérification de correction des démonstrations, 8