Advertisement

Deduction and computation

  • Gérard Huet
Part Two Knowledge Processing
Part of the Lecture Notes in Computer Science book series (LNCS, volume 232)

Keywords

Inference System Inference Rule Critical Pair Natural Deduction Proof Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    A. Aho, J. Hopcroft, J. Ullman. “The Design and Analysis of Computer Algorithms.” Addison-Wesley (1974).Google Scholar
  2. [2]
    P. B. Andrews. “Resolution in Type Theory.” Journal of Symbolic Logic 36,3 (1971), 414–432.Google 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).Google 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.Google 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).Google 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.Google 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 hommemachine 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).Google 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).Google 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.CrossRefGoogle Scholar
  41. [41]
    Dummett. “Elements of Intuitionism.” Clarendon Press, Oxford (1977).Google 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.Google 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).Google 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. “Uber 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.CrossRefGoogle 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).Google 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.CrossRefGoogle 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.CrossRefGoogle Scholar
  63. [63]
    G. Huet. “A Unification Algorithm for Typed Lambda Calculus.” Theoretical Computer Science, 1.1 (1975) 27–57.CrossRefGoogle Scholar
  64. [64]
    G. Huct. “Résolution d'équations dans des langages d'ordre 1,2, ... ω.” 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.Google Scholar
  66. [66]
    G. Huet. “A Complete Proof of Correctness of the Knuth-Bendix 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.Google 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 (Déc. 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. Leech Ed., 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.CrossRefGoogle 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.Google Scholar
  89. [89]
    P. J. Landin. “The next 700 programming languages.” Comm. ACM 9,3 (1966) 157–166.CrossRefGoogle Scholar
  90. [90]
    Philippe Le Chenadec. “Formes canoniques dans les algèbres finiment présentées.” 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. Lévy. “Réductions correctes et optimales dans le λ-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. MacQueen, 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).Google 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.CrossRefGoogle Scholar
  101. [101]
    William A. Martin. “Determining the equivalence of algebraic expressions by hash coding.” JACM 18,4 (1971) 549–558.CrossRefGoogle 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).Google Scholar
  107. [107]
    J. Mć 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.CrossRefGoogle 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.CrossRefGoogle Scholar
  116. [116]
    M.H.A. Newman. “On Theories with a Combinatorial Definition of “Equivalence”.” Annals of Math. 43,2 (1942) 223–243.Google 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.CrossRefGoogle Scholar
  121. [121]
    A. Obtulowicz. “The Logic of Categories of Partial Functions and its Applications.” Dissertationes 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.CrossRefGoogle 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.E. Stickel. “Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms.” JACM 28,2 (1981) 233–264.CrossRefGoogle Scholar
  128. [128]
    T. Pietrzykowski, D.C. Jensen. “A complete mechanization of ω-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.CrossRefGoogle Scholar
  130. [130]
    D. Prawitz. “Natural Deduction.” Almqist and Wiskell, Stockolm (1965).Google 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 tom 41, PWN, Polish Scientific Publishers, Warszawa (1963).Google 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.CrossRefGoogle 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).Google Scholar
  144. [144]
    R.E. Shostak “Deciding Combinations of Theories.” JACM 31,1 (1985) 1–12.CrossRefGoogle 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.CrossRefGoogle Scholar
  148. [148]
    R. Statman. “The typed Lambda-Calculus is not Elementary Recursive.” Theoretical Computer Science 9 (1979) 73–81.CrossRefGoogle Scholar
  149. [149]
    S. Stenlund. “Combinators λ-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.CrossRefGoogle Scholar
  151. [151]
    M.E. Szabo. “Algebra of Proofs.” North-Holland (1978).Google 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 I.” J. of Symbolic Logic 32 (1967) 198–212.Google 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.CrossRefGoogle Scholar
  159. [159]
    R. E. Tarjan, J. van Leeuwen. “Worst-case Analysis of Set Union Algorithms.” JACM 31,2 (1985) 245–281.CrossRefGoogle Scholar
  160. [160]
    A. Tarski. “A lattice-theoretical fixpoint theorem and its applications.” Pacific J. Math. 5 (1955) 285–309.Google 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 λ-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 1986

Authors and Affiliations

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

Personalised recommendations