Deduction and Computation

  • Gérard Huet
Part of the Springer Study Edition book series (SSE)


We present in a unified framework the basic syntactic notions of deduction and computation.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Aho, J. Hopcroft, J. Ullman. “The Design and Analysis of Computer Algorithms.” Addison-Wesley (1974).zbMATHGoogle Scholar
  2. [2]
    P. B. Andrews. “Resolution in Type Theory.” Journal of Symbolic Logic 36,3 (1971), 414–432.zbMATHMathSciNetGoogle Scholar
  3. [3]
    P. B. Andrews, D. A. Miller, E. L. Cohen, F. Pfenning. “Automating higher-order logic.” Dept of Math, University Carnegie-Mellon, (Jan. 1983).Google Scholar
  4. [4]
    H. Barendregt. “The Lambda-Calculus: Its Syntax and Semantics.” North-Holland (1980).Google Scholar
  5. [5]
    E. Bishop. “Foundations of Constructive Analysis.” McGraw-Hill, New-York (1967).zbMATHGoogle Scholar
  6. [6]
    E. Bishop. “Mathematics as a numerical language.” Intuitionism and Proof Theory, Eds. J. Myhill, A.Kino and R.E.Vesley, North-Holland, Amsterdam, (1970) 53–71.Google Scholar
  7. [7]
    C. Böhm, A. Berarducci. “Automatic Synthesis of Typed Lambda-Programs on Term Algebras.” Unpublished manuscript, (June 1984).Google Scholar
  8. [8]
    R.S. Boyer, J Moore. “The sharing of structure in theorem proving programs.” Machine Intelligence 7 (1972) Edinburgh U. Press, 101–116.zbMATHGoogle Scholar
  9. [9]
    R. Boyer, J Moore. “A Lemma Driven Automatic Theorem Prover for Recursive Function Theory.” 5th International Joint Conference on Artificial Intelligence, (1977) 511–519.Google Scholar
  10. [10]
    R. Boyer, J Moore. “A Computational Logic.” Academic Press (1979).zbMATHGoogle Scholar
  11. [11]
    R. Boyer, J Moore. “A mechanical proof of the unsolvability of the halting problem.” Report ICSCA-CMP-28, Institute for Computing Science, University of Texas at Austin (July 1982).Google Scholar
  12. [12]
    R. Boyer, J Moore. “Proof Checking the RSA Public Key Encryption Algorithm.” Report ICSCA-CMP-33, Institute for Computing Science, University of Texas at Austin (Sept. 1982).Google Scholar
  13. [13]
    R. Boyer, J Moore. “Proof checking theorem proving and program verification.” Report ICSCA-CMP-35, Institute for Computing Science, University of Texas at Austin (Jan. 1983).Google Scholar
  14. [14]
    N.G. de Bruijn. “The mathematical language AUTOMATH, its usage and some of its extensions.” Symposium on Automatic Demonstration, IRIA, Versailles, 1968. Printed as Springer-Verlag Lecture Notes in Mathematics 125, (1970) 29–61.Google Scholar
  15. [15]
    N.G. de Bruijn. “Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.” Indag. Math. 34,5 (1972), 381–392.Google Scholar
  16. [16]
    N.G. de Bruijn. “Automath a language for mathematics.” Les Presses de l’Université de Montréal, (1973).Google Scholar
  17. [17]
    N.G. de Bruijn. “Some extensions of Automath: the AUT-4 family.” Internal Automath memo M10 (Jan. 1974).Google Scholar
  18. [18]
    N.G. de Bruijn. “A survey of the project Automath.” (1980) in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds Seldin J. P. and Hindley J. R., Academic Press (1980).Google Scholar
  19. [19]
    M. Bruynooghe. “The Memory Management of PROLOG implementations.” Logic Programming Workshop. Ed. Tarnlund S.A (July 1980).Google Scholar
  20. [20]
    L. Cardelli. “ML under UNIX.” Bell Laboratories, Murray Hill, New Jersey (1982).Google Scholar
  21. [21]
    L. Cardelli. “Amber.” Bell Laboratories, Murray Hill, New Jersey (1985).Google Scholar
  22. [22]
    A. Church. “A formulation of the simple theory of types.” Journal of Symbolic Logic 5,1 (1940) 56–68.MathSciNetGoogle Scholar
  23. [23]
    A. Church. “The Calculi of Lambda-Conversion.” Princeton U. Press, Princeton N.J. (1941).Google Scholar
  24. [24]
    A. Colmerauer, H. Kanoui, R. Pasero, Ph. Roussel. “Un système de communication homme-machine en francais.” Rapport de recherche, Groupe Intelligence Artificielle, Faculté des Sciences de Luminy, Marseille (1973).Google Scholar
  25. [25]
    R.L. Constable, J.L. Bates. “Proofs as Programs.” Dept. of Computer Science, Cornell University. (Feb. 1983).Google Scholar
  26. [26]
    R.L. Constable, J.L. Bates. “The Nearly Ultimate Pearl.” Dept. of Computer Science, Cornell University. (Dec. 1983).Google Scholar
  27. [27]
    Th. Coquand. “Une théorie des constructions.” Thèse de troisième cycle, Université Paris VII (Jan. 85).Google Scholar
  28. [28]
    Th. Coquand, G. Huet. “A Theory of Constructions.” Preliminary version, presented at the International Symposium on Semantics of Data Types, Sophia-Antipolis (June 84).Google Scholar
  29. [29]
    Th. Coquand, G. Huet.“Constructions: A Higher Order Proof System for Mechanizing Mathematics.” EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).Google Scholar
  30. [30]
    Th. Coquand, G. Huet. “Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions.” Colloque de Logique, Orsay (Juil. 1985).Google Scholar
  31. [31]
    Th. Coquand, G. Huet. “A Calculus of Constructions.” To appear, JCSS (1986).Google Scholar
  32. [32]
    J. Corbin, M. Bidoit. “A Rehabilitation of Robinson’s Unification Algorithm.” IFIP 83, Elsevier Science (1983) 909–914.Google Scholar
  33. [33]
    G. Cousineau, P.L. Curien and M. Mauny. “The Categorical Abstract Machine.” In Functional Programming Languages and Computer Architecture, Ed. J. P. Jouannaud, Springer-Verlag LNCS 201 (1985) 50–64.Google Scholar
  34. [34]
    P.L. Curien. “Combinateurs catégoriques, algorithmes séquentiels et programmation applicative.” Thèse de Doctorat d’Etat, Université Paris VII (Dec. 1983).Google Scholar
  35. [35]
    P. L. Curien. “Categorical Combinatory Logic.” ICALP 85, Nafplion, Springer-Verlag LNCS 194 (1985).Google Scholar
  36. [36]
    P.L. Curien. “Categorical Combinators, Sequential Algorithms and Functional Programming.” Pitman (1986).zbMATHGoogle Scholar
  37. [37]
    H. B. Curry, R. Feys. “Combinatory Logic Vol. I.” North-Holland, Amsterdam (1958).Google Scholar
  38. [38]
    D. Van Daalen. “The language theory of Automath.” Ph. D. Dissertation, Technological Univ. Eindhoven (1980).zbMATHGoogle Scholar
  39. [39]
    Luis Damas, Robin Milner. “Principal type-schemas for functional programs.” Edinburgh University (1982).Google Scholar
  40. [40]
    P.J. Downey, R. Sethi, R. Tarjan. “Variations on the common subexpression problem.” JACM 27,4 (1980) 758–771.zbMATHMathSciNetGoogle Scholar
  41. [41]
    Dummett. “Elements of Intuitionism.” Clarendon Press, Oxford (1977).zbMATHGoogle Scholar
  42. [42]
    F. Fages. “Formes canoniques dans les algèbres booléennes et application à la démonstration automatique en logique de premier ordre.” Thèse de 3ème cycle, Univ. de Paris VI (Juin 1983).Google Scholar
  43. [43]
    F. Fages. “Associative-Commutative Unification.” Submitted for publication (1985).Google Scholar
  44. [44]
    F. Fages, G. Huet. “Unification and Matching in Equational Theories.” CAAP 83, l’Aquila, Italy. In Springer-Verlag LNCS 159 (1983).Google Scholar
  45. [45]
    P. Flajolet, J.M. Steyaert. “On the Analysis of Tree-Matching Algorithms.” in Automata, Languages and Programming 7th Int. Coll., Lecture Notes in Computer Science 85 Springer Verlag (1980) 208–219.Google Scholar
  46. [46]
    S. Fortune, D. Leivant, M. O’Donnell. “The Expressiveness of Simple and Second-Order Type Structures.” Journal of the Assoc. for Comp. Mach., 30,1, (Jan. 1983) 151–185.zbMATHMathSciNetGoogle Scholar
  47. [47]
    G. Frege. “Begriffschrift, a formula language, modeled upon that of arithmetic, for pure thought.” (1879). Reprinted in From Frege to Gödel, J. van Heijenoort, Harvard University Press, 1967.Google Scholar
  48. [48]
    G. Gentzen. “The Collected Papers of Gerhard Gentzen.” Ed. E. Szabo, North-Holland, Amsterdam (1969).zbMATHGoogle Scholar
  49. [49]
    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. Proceedings of the Second Scandinavian Logic Symposium, Ed. J.E. Fenstad, North Holland (1970) 63–92.Google Scholar
  50. [50]
    J.Y. Girard. “Interprétation fonctionnelle et élimination des coupures dans l’arithmétique d’ordre supérieure.” Thèse d’Etat, Université Paris VII (1972).Google Scholar
  51. [51]
    K. Gödel. “Über eine bisher noch nicht benutze Erweitrung des finiten Standpunktes.” Dialectica, 12 (1958).Google Scholar
  52. [52]
    W. D. Goldfarb. “The Undecidability of the Second-order Unification Problem.” Theoretical Computer Science, 13, (1981) 225–230.zbMATHMathSciNetGoogle Scholar
  53. [53]
    M. Gordon, R. Milner, C. Wadsworth. “A Metalanguage for Interactive Proof in LCF.” Internal Report CSR-16–77, Department of Computer Science, University of Edinburgh (Sept. 1977).Google Scholar
  54. [54]
    M. J. Gordon, A. J. Milner, C. P. Wadsworth. “Edinburgh LCF” Springer-Verlag LNCS 78 (1979).zbMATHGoogle Scholar
  55. [55]
    W. E. Gould. “A Matching Procedure for Omega Order Logic.” Scientific Report 1, AFCRL 66–781, contract AF19 (628)-3250 (1966).Google Scholar
  56. [56]
    J. Guard. “Automated Logic for Semi-Automated Mathematics.” Scientific Report 1, AFCRL (1964).Google Scholar
  57. [57]
    J. Herbrand. “Recherches sur la théorie de la démonstration.” Thèse, U. de Paris (1930). In: Ecrits logiques de Jacques Herbrand, PUF Paris (1968).Google Scholar
  58. [58]
    C. M. Hoffmann, M. J. O’Donnell. “Programming with Equations.” ACM Transactions on Programming Languages and Systems, 4,1 (1982) 83–112.zbMATHMathSciNetGoogle Scholar
  59. [59]
    W. A. Howard. “The formulæ-as-types notion of construction.” Unpublished manuscript (1969). Reprinted in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds Seldin J. P. and Hindley J. R., Academic Press (1980).Google Scholar
  60. [60]
    G. Huet. “Constrained Resolution: a Complete Method for Type Theory.” Ph.D. Thesis, Jennings Computing Center Report 1117, Case Western Reserve University (1972).Google Scholar
  61. [61]
    G. Huet. “A Mechanization of Type Theory.” Proceedings, 3rd IJCAI, Stanford (Aug. 1973).Google Scholar
  62. [62]
    G. Huet. “The Undecidability of Unification in Third Order Logic.” Information and Control 22 (1973) 257–267.zbMATHMathSciNetGoogle Scholar
  63. [63]
    G. Huet. “A Unification Algorithm for Typed Lambda Calculus.” Theoretical Computer Science, 1.1 (1975) 27–57.MathSciNetGoogle Scholar
  64. [64]
    G. Huet. “Résolution d’équations dans des langages d’ordre 1,2,... w.” Thèse d’Etat, Université Paris VII (1976).Google Scholar
  65. [65]
    G. Huet. “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems.” J. Assoc. Comp. Mach. 27,4 (1980) 797–821.zbMATHMathSciNetGoogle Scholar
  66. [66]
    G. Huet. “A Complete Proof of Correctness of the Knuth-Bcndix Completion Algorithm.” JCSS 23,1 (1981) 11–21.Google Scholar
  67. [67]
    G. Huet. “Initiation à la Théorie des Catégories.” Polycopié de cours de DEA, Université Paris VII (Nov. 1985).Google Scholar
  68. [68]
    G. Huet. “Cartesian Closed Categories and Lambda-Calculus.” Category Theory Seminar, Carnegie-Mellon University (Dec. 1985).Google Scholar
  69. [69]
    G. Huet, J.M. Hullot. “Proofs by Induction in Equational Theories With Constructors.” JACM 25,2 (1982) 239–266.zbMATHMathSciNetGoogle Scholar
  70. [70]
    G. Huet, J.J. Lévy “Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems.” Rapport Laboria 359, IRIA (Aug. 1979).Google Scholar
  71. [71]
    G. Huet, D. Oppen. “Equations and Rewrite Rules: a Survey.” In Formal Languages: Perspectives and Open Problems, Ed. Book R., Academic Press (1980).Google Scholar
  72. [72]
    J.M. Hullot “Compilation de Formes Canoniques dans les Théories Equationnelles.” Thèse de 3ème cycle, U. de Paris Sud (Nov. 80).Google Scholar
  73. [73]
    Jean Pierre Jouannaud, Helene Kirchner. “Completion of a set of rules modulo a set of equations.” (April 1984).Google Scholar
  74. [74]
    L.S. Jutting. “A translation of Landau’s “Grundlagen” in AUTOMATH.” Eindhoven University of Technology, Dept of Mathematics (Oct. 1976).Google Scholar
  75. [75]
    L.S. van Benthem Jutting. “The language theory of ∧, a typed λ-calculus where terms are types.” Unpublished manuscript (1984).Google Scholar
  76. [76]
    G. Kahn, G. Plotkin. “Domaines concrets.” Rapport Laboria 336, IRIA (Dec. 1978).Google Scholar
  77. [77]
    J. Ketonen, J. S. Weening. “The language of an interactive proof checker.” Stanford University (1984).Google Scholar
  78. [78]
    J. Ketonen. “EKL-A Mathematically Oriented Proof Checker.” 7th International Conference on Automated Deduction, Napa, California (May 1984). Springer-Verlag LNCS 170.Google Scholar
  79. [79]
    J. Ketonen. “A mechanical proof of Ramsey theorem.” Stanford Univ. (1983).Google Scholar
  80. [80]
    S.C. Kleene. “Introduction to Meta-mathematics.” North Holland (1952).Google Scholar
  81. [81]
    S.C. Kleene. “On the interpretation of intuitionistic number theory.” J. Symbolic Logic 31 (1945).Google Scholar
  82. [82]
    S.C. Kleene. “On the interpretation of intuitionistic number theory.” J. Symbolic Logic 31 (1945).Google Scholar
  83. [83]
    J.W. Klop. “Combinatory Reduction Systems.” Ph. D. Thesis, Mathematisch Centrum Amsterdam (1980).Google Scholar
  84. [84]
    D. Knuth, P. Bendix. “Simple word problems in universal algebras”. In: Computational Problems in Abstract Algebra, J. LeechEd., Pergamon (1970) 263–297.Google Scholar
  85. [85]
    D.E. Knuth, J. Morris, V. Pratt. “Fast Pattern Matching in Strings.” SIAM Journal on Computing 6,2 (1977) 323–350.zbMATHMathSciNetGoogle Scholar
  86. [86]
    G. Kreisel. “On the interpretation of nonfinitist proofs, Part I, II.” JSL 16 (1952, 1953).Google Scholar
  87. [87]
    J. Lambek. “From Lambda-calculus to Cartesian Closed Categories.” in To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Eds. J. P. Seldin and J. R. Hindley, Academic Press (1980).Google Scholar
  88. [88]
    J. Lambek and P. J. Scott. “Aspects of Higher Order Categorical Logic.” Contemporary Mathematics 30 (1984) 145–174.MathSciNetGoogle Scholar
  89. [89]
    P. J. Landin. “The next 700 programming languages.” Comm. ACM 9,3 (1966) 157–166.zbMATHGoogle Scholar
  90. [90]
    Philippe Le Chenadec. “Formes canoniques dans les algèbres finiment presentees.” Thèse de 3ème cycle, Univ. d’Orsay (Juin 1983).Google Scholar
  91. [91]
    D. Leivant. “Polymorphic type inference.” 10th ACM Conference on Principles of Programming Languages (1983).Google Scholar
  92. [92]
    D. Leivant. “Structural semantics for polymorphic data types.” 10th ACM Conference on Principles of Programming Languages (1983).Google Scholar
  93. [93]
    J.J. Levy. “Réductions correctes et optimales dans le A-calcul.” Thèse d’Etat, U. Paris VII (1978).Google Scholar
  94. [94]
    S. MacLane. “Categories for the Working Mathematician.” Springer-Verlag (1971).Google Scholar
  95. [95]
    D. Mac Queen, G. Plotkin, R. Sethi. “An ideal model for recursive polymorphic types.” Proceedings, Principles of Programming Languages Symposium, Jan. 1984, 165–174.Google Scholar
  96. [96]
    D. B. MacQueen, R. Sethi. “A semantic model of types for applicative languages.” ACM Symposium on Lisp and Functional Programming (Aug. 1982).Google Scholar
  97. [97]
    E.G. Manes. “Algebraic Theories.” Springer-Verlag (1976).zbMATHGoogle Scholar
  98. [98]
    C. Mann. “The Connection between Equivalence of Proofs and Cartesian Closed Categories.” Proc. London Math. Soc. 31 (1975) 289–310.Google Scholar
  99. [99]
    A. Martelli, U. Montanari. “Theorem proving with structure sharing and efficient unification.” Proc. 5th IJCAI, Boston, (1977) p 543.Google Scholar
  100. [100]
    A. Martelli, U. Montanari. “An Efficient Unification Algorithm.” ACM Trans. on Prog. Lang. and Syst. 4,2 (1982) 258–282.zbMATHGoogle Scholar
  101. [101]
    William A. Martin. “Determining the equivalence of algebraic expressions by hash coding.” JACM 18,4 (1971) 549–558.zbMATHGoogle Scholar
  102. [102]
    P. Martin-Löf. “A theory of types.” Report 71–3, Dept. of Mathematics, University of Stockholm, Feb. 1971, revised (Oct. 1971).Google Scholar
  103. [103]
    P. Martin-Löf. “About models for intuitionistic type theories and the notion of definitional equality.” Paper read at the Orléans Logic Conference (1972).Google Scholar
  104. [104]
    P. Martin-Löf. “An intuitionistic Theory of Types: predicative part.” Logic Colloquium 73, Eds. H. Rose and J. Sepherdson, North-Holland, (1974) 73–118.Google Scholar
  105. [105]
    P. Martin-Löf. “Constructive Mathematics and Computer Programming.” In Logic, Methodology and Philosophy of Science 6 (1980) 153–175, North-Holland.Google Scholar
  106. [106]
    P. Martin-Löf. “Intuitionistic Type Theory.” Studies in Proof Theory, Bibliopolis (1984).zbMATHGoogle Scholar
  107. [107]
    J. Mc Carthy. “Recursive functions of symbolic expressions and their computation by machine.” CACM 3,4 (1960) 184–195.Google Scholar
  108. [108]
    N. McCracken. “An investigation of a programming language with a polymorphic type structure.” Ph.D. Dissertation, Syracuse University (1979).Google Scholar
  109. [109]
    D.A. Miller. “Proofs in Higher-order Logic.” Ph. D. Dissertation, Carnegie-Mellon University (Aug. 1983).Google Scholar
  110. [110]
    D.A. Miller. “Expansion tree proofs and their conversion to natural deduction proofs.” Technical report MS-CIS-84–6, University of Pennsylvania (Feb. 1984).Google Scholar
  111. [111]
    R. Milner. “A Theory of Type Polymorphism in Programming.” Journal of Computer and System Sciences 17 (1978) 348–375.zbMATHMathSciNetGoogle Scholar
  112. [112]
    R. Milner. “A proposal for Standard ML.” Report CSR-157–83, Computer Science Dept., University of Edinburgh (1983).Google Scholar
  113. [113]
    R.P. Nederpelt. “Strong normalization in a typed À calculus with À structured types.” Ph. D. Thesis, Eindhoven University of Technology (1973).Google Scholar
  114. [114]
    R.P. Nederpelt. “An approach to theorem proving on the basis of a typed λ-calculus.” 5th Conference on Automated Deduction, Les Arcs, France. Springer-Verlag LNCS 87 (1980).Google Scholar
  115. [115]
    G. Nelson, D.C. Oppen. “Fast decision procedures based on congruence closure.” JACM 27,2 (1980) 356–364.zbMATHMathSciNetGoogle Scholar
  116. [116]
    M.H.A. Newman. “On Theories with a Combinatorial Definition of “Equivalence”.” Annals of Math. 43,2 (1942) 223–243.zbMATHGoogle Scholar
  117. [117]
    B. Nordström. “Programming in Constructive Set Theory: Some Examples.” Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture, Portmouth, New Hampshire (Oct. 1981) 141–154.Google Scholar
  118. [118]
    B. Nordström. “Description of a Simple Programming Language.” Report 1, Programming Methodology Group, University of Goteborg (Apr. 1984).Google Scholar
  119. [119]
    B. Nordström, K. Petersson. “Types and Specifications.” Information Processing 83, Ed. R. Mason, North-Holland, (1983) 915–920.Google Scholar
  120. [120]
    B. Nordström, J. Smith. “Propositions and Specifications of Programs in Martin-Löf’s Type Theory.” BIT 24, (1984) 288–301.Google Scholar
  121. [121]
    A. Obtulowicz. “The Logic of Categories of Partial Functions and its Applications.” Disser-tationes Mathematicae 241 (1982).Google Scholar
  122. [122]
    M.S. Paterson, M.N. Wegman. “Linear Unification.” J. of Computer and Systems Sciences 16 (1978) 158–167.zbMATHMathSciNetGoogle Scholar
  123. [123]
    L. Paulson. “Recent Developments in LCF: Examples of structural induction.” Technical Report No 34, Computer Laboratory, University of Cambridge (Jan. 1983).Google Scholar
  124. [124]
    L. Paulson. “Tactics and Tacticals in Cambridge LCF.” Technical Report No 39, Computer Laboratory, University of Cambridge (July 1983).Google Scholar
  125. [125]
    L. Paulson. “Verifying the unification algorithm in LCF.” Technical report No 50, Computer Laboratory, University of Cambridge (March 1984).Google Scholar
  126. [126]
    L. C. Paulson. “Constructing Recursion Operators in Intuitionistic Type Theory.” Tech. Report 57, Computer Laboratory, University of Cambridge (Oct. 1984).Google Scholar
  127. [127]
    G.E. Peterson, M.É. Stickel. “Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms.” JACM 28,2 (1981) 233–264.zbMATHMathSciNetGoogle Scholar
  128. [128]
    T. Pietrzykowski, D.C. Jensen. “A complete mechanization of w-order type theory.” Proceedings of ACM Annual Conference (1972).Google Scholar
  129. [129]
    T. Pietrzykowski. “A Complete Mechanization of Second-Order Type Theory.” JACM 20 (1973) 333–364.zbMATHMathSciNetGoogle Scholar
  130. [130]
    D. Prawitz. “Natural Deduction.” Almqist and Wiskell, Stockolm (1965).zbMATHGoogle Scholar
  131. [131]
    D. Prawitz. “Ideas and results in proof theory.” Proceedings of the Second Scandinavian Logic Symposium (1971).Google Scholar
  132. [132]
    PRL staff. “Implementing Mathematics with the NUPRL Proof Development System.” Computer Science Department, Cornell University (May 1985).Google Scholar
  133. [133]
    H. Rasiowa, R. Sikorski“The Mathematics of Metamathematics.” Monografie Matematyczne torn 41, PWN, Polish Scientific Publishers, Warszawa (1963).zbMATHGoogle Scholar
  134. [134]
    J. C. Reynolds. “Definitional Interpreters for Higher Order Programming Languages.” Proc. ACM National Conference, Boston, (Aug. 72) 717–740.Google Scholar
  135. [135]
    J. C. Reynolds. “Towards a Theory of Type Structure.” Programming Symposium, Paris. Springer Verlag LNCS 19 (1974) 408–425.Google Scholar
  136. [136]
    J. C. Reynolds. “Types, abstraction, and parametric polymorphism.” IFIP Congress’83, Paris (Sept. 1983).Google Scholar
  137. [137]
    J. C. Reynolds. “Polymorphism is not set-theoretic.” International Symposium on Semantics of Data Types, Sophia-Antipolis (June 1984).Google Scholar
  138. [138]
    J. C. Reynolds. “Three approaches to type structure.” TAPSOFT Advanced Seminar on the Role of Semantics in Software Development, Berlin (March 1985).Google Scholar
  139. [139]
    J. A. Robinson. “A Machine-Oriented Logic Based on the Resolution Principle.” JACM 12 (1965) 32–41.Google Scholar
  140. [140]
    J. A. Robinson. “Computational Logic: the Unification Computation.” Machine Intelligence 6 Eds B. Meltzer and D.Michie, American Elsevier, New-York (1971).Google Scholar
  141. [141]
    D. Scott. “Constructive validity.” Symposium on Automatic Demonstration, Springer-Verlag Lecture Notes in Mathematics, 125 (1970).Google Scholar
  142. [142]
    D. Scott.“Relating Theories of the Lambda-Calculus.” in To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Eds. J. P. Seldin and J. R. Hindley, Academic Press (1980).Google Scholar
  143. [143]
    J.R. Shoenfield. “Mathematical Logic.” Addison-Wesley (1967).zbMATHGoogle Scholar
  144. [144]
    R.E. Shostak“Deciding Combinations of Theories.” JACM 31,1 (1985) 1–12.MathSciNetGoogle Scholar
  145. [145]
    J. Smith. “Course-of-values recursion on lists in intuitionistic type theory.” Unpublished notes, Göteborg University (Sept. 1981).Google Scholar
  146. [146]
    J. Smith. “The identification of propositions and types in Martin-Lof’s type theory: a programming example.” International Conference on Foundations of Computation Theory, Borgholm, Sweden, (Aug. 1983) Springer-Verlag LNCS 158.Google Scholar
  147. [147]
    R. Statman. “Intuitionistic Propositional Logic is Polynomial-space Complete.” Theoretical Computer Science 9 (1979) 67–72, North-Holland.Google Scholar
  148. [148]
    R. Statman. “The typed Lambda-Calculus is not Elementary Recursive.” Theoretical Computer Science 9 (1979) 73–81.zbMATHMathSciNetGoogle Scholar
  149. [149]
    S. Stenlund. “Combinators A-terms, and proof theory.” Reidel (1972).Google Scholar
  150. [150]
    M.E. Stickel“A Complete Unification Algorithm for Associative-Commutative Functions.” JACM 28,3 (1981) 423–434.zbMATHMathSciNetGoogle Scholar
  151. [151]
    M.E. Szabo. “Algebra of Proofs.” North-Holland (1978).zbMATHGoogle Scholar
  152. [152]
    W. Tait. “A non constructive proof of Gentzen’s Hauptsatz for second order predicate logic.” Bull. Amer. Math. Soc. 72 (1966).Google Scholar
  153. [153]
    W. Tait. “Intensional interpretations of functionals of finite type L” J. of Symbolic Logic 32 (1967) 198–212.zbMATHMathSciNetGoogle Scholar
  154. [154]
    W. Tait. “A Realizability Interpretation of the Theory of Species.” Logic Colloquium, Ed. R. Parikh, Springer Verlag Lecture Notes 453 (1975).Google Scholar
  155. [155]
    M. Takahashi. “A proof of cut-elimination theorem in simple type theory.” J. Math. Soc. Japan 19 (1967).Google Scholar
  156. [156]
    G. Takeuti. “On a generalized logic calculus.” Japan J. Math. 23 (1953).Google Scholar
  157. [157]
    G. Takeuti. “Proof theory.” Studies in Logic 81 Amsterdam (1975).Google Scholar
  158. [158]
    R. E. Tarjan. “Efficiency of a good but non linear set union algorithm.” JACM 22,2 (1975) 215–225.zbMATHMathSciNetGoogle Scholar
  159. [159]
    R. E. Tarjan, J. van Leeuwen. “Worst-case Analysis of Set Union Algorithms.” JACM 31,2 (1985) 245–281.Google Scholar
  160. [160]
    A. Tarski. “A lattice-theoretical fixpoint theorem and its applications.” Pacific J. Math. 5 (1955) 285–309.zbMATHMathSciNetGoogle Scholar
  161. [161]
    D.A. Turner. “Miranda: A non-strict functional language with polymorphic types.” In Functional Programming Languages and Computer Architecture, Ed. J. P. Jouannaud, Springer-Verlag LNCS 201 (1985) 1–16.Google Scholar
  162. [162]
    R. de Vrijer “Big Trees in a λ-calculus with λ-expressions as types.” Conference on A-calculus and Computer Science Theory, Rome, Springer-Verlag LNCS 37 (1975) 252–271.Google Scholar
  163. [163]
    D. Warren“Applied Logic — Its use and implementation as a programming tool.” Ph.D. Thesis, University of Edinburgh (1977).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1987

Authors and Affiliations

  • Gérard Huet
    • 1
  1. 1.INRIA and CMUUSA

Personalised recommendations