Skip to main content
SpringerLink
Log in

Deduction and Computation

  • Conference paper
Logic of Programming and Calculi of Discrete Design

Part of the book series: NATO ASI Series ((NATO ASI F,volume 36))

Abstract

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

A preliminary version of these course notes was presented at the Advanced Course in Artificial Intelligence held in Vignieu (France) in July 1985, and appeared in “Fundamentals in Artificial Intelligence”, Eds. W. Bibel and Ph. Jorrand, Springer-Verlag Lecture Notes in Computer Science vol. 232.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Aho, J. Hopcroft, J. Ullman. “The Design and Analysis of Computer Algorithms.” Addison-Wesley (1974).

    MATH  Google Scholar 

  2. P. B. Andrews. “Resolution in Type Theory.” Journal of Symbolic Logic 36,3 (1971), 414–432.

    MathSciNet  MATH  Google Scholar 

  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. H. Barendregt. “The Lambda-Calculus: Its Syntax and Semantics.” North-Holland (1980).

    Google Scholar 

  5. E. Bishop. “Foundations of Constructive Analysis.” McGraw-Hill, New-York (1967).

    MATH  Google Scholar 

  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. C. Böhm, A. Berarducci. “Automatic Synthesis of Typed Lambda-Programs on Term Algebras.” Unpublished manuscript, (June 1984).

    Google Scholar 

  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. 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. R. Boyer, J Moore. “A Computational Logic.” Academic Press (1979).

    MATH  Google Scholar 

  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. 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. 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. 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. 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. N.G. de Bruijn. “Automath a language for mathematics.” Les Presses de l’Université de Montréal, (1973).

    MATH  Google Scholar 

  17. N.G. de Bruijn. “Some extensions of Automath: the AUT-4 family.” Internal Automath memo MIO (Jan. 1974).

    Google Scholar 

  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. M. Bruynooghe. “The Memory Management of PROLOG implementations.” Logic Programming Workshop. Ed. Tarnlund S.A (July 1980).

    Google Scholar 

  20. L. Cardelli. “ML under UNIX.” Bell Laboratories, Murray Hill, New Jersey (1982).

    Google Scholar 

  21. L. Cardelli. “Amber.” Bell Laboratories, Murray Hill, New Jersey (1985).

    Google Scholar 

  22. D. de Champeaux. “About the Paterson-Wegman Linear Unification Algorithm.” J. of Comp. and System Sciences 32 (1986) 79–90.

    MATH  Google Scholar 

  23. A. Church. “A formulation of the simple theory of types.” Journal of Symbolic Logic 5,1 (1940) 56–68.

    MathSciNet  MATH  Google Scholar 

  24. A. Church. “The Calculi of Lambda-Conversion.” Princeton U. Press, Princeton N.J. (1941).

    Google Scholar 

  25. 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 

  26. R.L. Constable, J.L. Bates. “Proofs as Programs.” Dept. of Computer Science, Cornell University. (Feb. 1983).

    Google Scholar 

  27. R.L. Constable, J.L. Bates. “The Nearly Ultimate Pearl.” Dept. of Computer Science, Cornell University. (Dec. 1983).

    Google Scholar 

  28. R.L. Constable et al. “Implementing Mathematics in the NuPrl System.” Prentice-Hall (1986).

    Google Scholar 

  29. Th. Coquand. “Une théorie des constructions.” Thèse de troisième cycle, Université Paris VII (Jan. 85).

    Google Scholar 

  30. Th. Coquand. “An analysis of Girard’s paradox.” First Conference on Logic in Computer Science, Boston (June 1986).

    Google Scholar 

  31. 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 

  32. Th. Coquand, G. Huet. “Constructions: A Higher Order Proof System for Mechanizing Mathematics.” EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).

    Google Scholar 

  33. Th. Coquand, G. Huet. “Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions.” Colloque de Logique, Orsay (Juil. 1985).

    Google Scholar 

  34. Th. Coquand, G. Huet. “A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction.” J. Symbolic Computation (1985) 1 323–328.

    MathSciNet  MATH  Google Scholar 

  35. Th. Coquand, G. Huet. “The Calculus of Constructions.” To appear, JCSS (1986).

    Google Scholar 

  36. J. Corbin, M. Bidoit. “A Rehabilitation of Robinson’s Unification Algorithm.” IFIP 83, Elsevier Science (1983) 909–914.

    Google Scholar 

  37. 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 

  38. 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 

  39. P. L. Curien. “Categorical Combinatory Logic.” ICALP 85, Nafplion, Springer-Verlag LNCS 194 (1985).

    Google Scholar 

  40. P.L. Curien. “Categorical Combinators, Sequential Algorithms and Functional Programming.” Pitman (1986).

    MATH  Google Scholar 

  41. H. B. Curry, R. Feys. “Combinatory Logic Vol. I.” North-Holland, Amsterdam (1958).

    Google Scholar 

  42. D. Van Daalen. “The language theory of Automath.” Ph. D. Dissertation, Technological Univ. Eindhoven (1980).

    Google Scholar 

  43. Luis Damas, Robin Milner. “Principal type-schemas for functional programs.” Edinburgh University (1982).

    Google Scholar 

  44. P.J. Downey, R. Sethi, R. Tarjan. “Variations on the common subexpression problem.” JACM 27,4 (1980) 758–771.

    MathSciNet  MATH  Google Scholar 

  45. M. Dummett. “Elements of Intuitionism.” Clarendon Press, Oxford (1977).

    MATH  Google Scholar 

  46. 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 

  47. F. Fages. “Associative-Commutative Unification.” Submitted for publication (1985).

    Google Scholar 

  48. F. Fages, G. Huet. “Unification and Matching in Equational Theories.” CAAP 83, l’Aquila, Italy. In Springer-Verlag LNCS 159 (1983).

    Google Scholar 

  49. 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 

  50. 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.

    MathSciNet  MATH  Google Scholar 

  51. 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 

  52. G. Gentzen. “The Collected Papers of Gerhard Gentzen.” Ed. E. Szabo, North-Holland, Amsterdam (1969).

    MATH  Google Scholar 

  53. 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 

  54. 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 

  55. K. Gödel. “Uber eine bisher noch nicht benutze Erweitrung des finiten Standpunktes.” Dialectica, 12 (1958).

    Google Scholar 

  56. W. D. Goldfarb. “The Undecidability of the Second-order Unification Problem.” Theoretical Computer Science, 13, (1981) 225–230.

    MathSciNet  MATH  Google Scholar 

  57. 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 

  58. M. J. Gordon, A. J. Milner, C. P. Wadsworth. “Edinburgh LCF” Springer-Verlag LNCS 78 (1979).

    MATH  Google Scholar 

  59. W. E. Gould. “A Matching Procedure for Omega Order Logic.” Scientific Report 1, AFCRL 66–781, contract AF19 (628)-3250 (1966).

    Google Scholar 

  60. J. Guard. “Automated Logic for Semi-Automated Mathematics.” Scientific Report 1, AFCRL (1964).

    Google Scholar 

  61. 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 

  62. C. M. Hoffmann, M. J. O’Donnell. “Programming with Equations.” ACM Transactions on Programming Languages and Systems, 4,1 (1982) 83–112.

    MATH  Google Scholar 

  63. W. A. Howard. “The formulae-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 

  64. 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 

  65. G. Huet. “A Mechanization of Type Theory.” Proceedings, 3rd IJCAI, Stanford (Aug. 1973).

    Google Scholar 

  66. G. Huet. “The Undecidability of Unification in Third Order Logic.” Information and Control 22 (1973) 257–267.

    MathSciNet  MATH  Google Scholar 

  67. G. Huet. “A Unification Algorithm for Typed Lambda Calculus.” Theoretical Computer Science, 1.1 (1975) 27–57.

    MathSciNet  Google Scholar 

  68. G. Huet. “Résolution d’équations dans des langages d’ordre 1,2,… ω.” Thèse d’Etat, Université Paris VII (1976).

    Google Scholar 

  69. G. Huet. “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems.” J. Assoc. Comp. Mach. 27,4 (1980) 797–821.

    MathSciNet  MATH  Google Scholar 

  70. G. Huet. “A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm.” JCSS 23,1 (1981) 11–21.

    MathSciNet  MATH  Google Scholar 

  71. G. Huet. “Initiation à la Théorie des Catégories.” Polycopié de cours de DEA, Université Paris VII (Nov. 1985).

    Google Scholar 

  72. G. Huet. “Cartesian Closed Categories and Lambda-Calculus.” Category Theory Seminar, Carnegie-Mellon University (Dec. 1985).

    Google Scholar 

  73. G. Huet. “Formal Structures for Computation and Deduction.” In preparation.

    Google Scholar 

  74. G. Huet, J.M. Hullot. “Proofs by Induction in Equational Theories With Constructors.” JCSS 25,2 (1982) 239–266.

    MathSciNet  MATH  Google Scholar 

  75. 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 

  76. 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 

  77. 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 

  78. Jean Pierre Jouannaud, Helene Kirchner. “Completion of a set of rules modulo a set of equations.” CSL Technical Note, SRI International (April 1984). To appear, SIAM Journal on Computing.

    Google Scholar 

  79. L.S. Jutting. “A translation of Landau’s “Grundlagen” in AUTOMATH.” Eindhoven University of Technology, Dept of Mathematics (Oct. 1976).

    Google Scholar 

  80. L.S. van Benthem Jutting. “The language theory of ⋀∞, a typed λ-calculus where terms are types.” Unpublished manuscript (1984).

    Google Scholar 

  81. G. Kahn, G. Plotkin. “Domaines concrets.” Rapport Laboria 336, IRIA (Déc. 1978).

    Google Scholar 

  82. J. Ketonen, J. S. Weening. “The language of an interactive proof checker.” Stanford University (1984).

    Google Scholar 

  83. J. Ketonen. “EKL-A Mathematically Oriented Proof Checker.” 7th International Conference on Automated Deduction, Napa, California (May 1984). Springer-Verlag LNCS 170.

    Google Scholar 

  84. J. Ketonen. “A mechanical proof of Ramsey theorem.” Stanford Univ. (1983).

    Google Scholar 

  85. S.C. Kleene. “On the interpretation of intuitionistic number theory.” J. Symbolic Logic 10 (1945).

    Google Scholar 

  86. S.C. Kleene. “Introduction to Meta-mathematics.” North Holland (1952).

    Google Scholar 

  87. J.W. Klop. “Combinatory Reduction Systems.” Ph. D. Thesis, Mathematisch Centrum Amsterdam (1980).

    Google Scholar 

  88. 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 

  89. D.E. Knuth, J. Morris, V. Pratt. “Fast Pattern Matching in Strings.” SIAM Journal on Computing 6,2 (1977) 323–350.

    MathSciNet  MATH  Google Scholar 

  90. G. Kreisel. “On the interpretation of nonfinitist proofs, Part I, II.” JSL 16,17 (1952, 1953).

    Google Scholar 

  91. 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 

  92. J. Lambek and P. J. Scott. “Aspects of Higher Order Categorical Logic.” Contemporary Mathematics 30 (1984) 145–174.

    Google Scholar 

  93. P. J. Landin. “The next 700 programming languages.” Comm. ACM 9,3 (1966) 157–166.

    MATH  Google Scholar 

  94. 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 

  95. D. Leivant. “Polymorphic type inference.” 10th ACM Symposium on Principles of Programming Languages (1983).

    Google Scholar 

  96. D. Leivant. “Structural semantics for polymorphic data types.” 10th ACM Conference on Principles of Programming Languages (1983).

    Google Scholar 

  97. J.J. Lévy. “Réductions correctes et optimales dans le λ-calcul.” Thèse d’Etat, U. Paris VII (1978).

    Google Scholar 

  98. S. MacLane. “Categories for the Working Mathematician.” Springer-Verlag (1971).

    Google Scholar 

  99. 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 

  100. D. B. MacQueen, R. Sethi. “A semantic model of types for applicative languages.” ACM Symposium on Lisp and Functional Programming (Aug. 1982).

    Google Scholar 

  101. E.G. Manes. “Algebraic Theories.” Springer-Verlag (1976).

    MATH  Google Scholar 

  102. C. Mann. “The Connection between Equivalence of Proofs and Cartesian Closed Categories.” Proc. London Math. Soc. 31 (1975) 289–310.

    MathSciNet  MATH  Google Scholar 

  103. A. Martelli, U. Montanari. “Theorem proving with structure sharing and efficient unification.” Proc. 5th IJCAI, Boston, (1977) p 543.

    Google Scholar 

  104. A. Martelli, U. Montanari. “An Efficient Unification Algorithm.” ACM Trans, on Prog. Lang. and Syst. 4,2 (1982) 258–282.

    MATH  Google Scholar 

  105. William A. Martin. “Determining the equivalence of algebraic expressions by hash coding.” JACM 18,4 (1971) 549–558.

    MATH  Google Scholar 

  106. P. Martin-Löf. “A theory of types.” Report 71–3, Dept. of Mathematics, University of Stockholm, Feb. 1971, revised (Oct. 1971).

    Google Scholar 

  107. 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 

  108. 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 

  109. P. Martin-Löf. “Constructive Mathematics and Computer Programming.” In Logic, Methodology and Philosophy of Science 6 (1980) 153–175, North-Holland.

    Google Scholar 

  110. P. Martin-Löf. “Intuitionistic Type Theory.” Studies in Proof Theory, Bibliopolis (1984).

    MATH  Google Scholar 

  111. J. Mc Carthy. “Recursive functions of symbolic expressions and their computation by machine.” CACM 3,4 (1960) 184–195.

    Google Scholar 

  112. N. McCracken. “An investigation of a programming language with a polymorphic type structure.” Ph.D. Dissertation, Syracuse University (1979).

    Google Scholar 

  113. D.A. Miller. “Proofs in Higher-order Logic.” Ph. D. Dissertation, Carnegie-Mellon University (Aug. 1983).

    Google Scholar 

  114. 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 

  115. R. Milner. “A Theory of Type Polymorphism in Programming.” Journal of Computer and System Sciences 17 (1978) 348–375.

    MathSciNet  MATH  Google Scholar 

  116. R. Milner. “A proposal for Standard ML.” Report CSR-157–83, Computer Science Dept., University of Edinburgh (1983).

    Google Scholar 

  117. C. Mohring. “Algorithm Development in the Calculus of Constructions.” IEEE Symposium on Logic in Computer Science, Cambridge, Mass. (June 1986).

    Google Scholar 

  118. R.P. Nederpelt. “Strong normalization in a typed λ calculus with A structured types.” Ph. D. Thesis, Eindhoven University of Technology (1973).

    Google Scholar 

  119. 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 

  120. G. Nelson, D.C. Oppen. “Fast decision procedures based on congruence closure.” JACM 27,2 (1980) 356–364.

    MathSciNet  MATH  Google Scholar 

  121. M.H.A. Newman. “On Theories with a Combinatorial Definition of “Equivalence”.” Annals of Math. 43,2 (1942) 223–243.

    MATH  Google Scholar 

  122. 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 

  123. B. Nordström. “Description of a Simple Programming Language.” Report 1, Programming Methodology Group, University of Goteborg (Apr. 1984).

    Google Scholar 

  124. B. Nordström, K. Petersson. “Types and Specifications.” Information Processing 83, Ed. R. Mason, North-Holland, (1983) 915–920.

    Google Scholar 

  125. B. Nordström, J. Smith. “Propositions and Specifications of Programs in Martin-Löfs Type Theory.” BIT 24, (1984) 288–301.

    MathSciNet  MATH  Google Scholar 

  126. A. Obtulowicz. “The Logic of Categories of Partial Functions and its Applications.” Disser-tationes Mathematicae 241 (1982).

    Google Scholar 

  127. M.S. Paterson, M.N. Wegman. “Linear Unification.” J. of Computer and Systems Sciences 16 (1978) 158–167.

    MathSciNet  MATH  Google Scholar 

  128. L. Paulson. “Recent Developments in LCF: Examples of structural induction.” Technical Report No 34, Computer Laboratory, University of Cambridge (Jan. 1983).

    Google Scholar 

  129. L. Paulson. “Tactics and Tacticals in Cambridge LCF.” Technical Report No 39, Computer Laboratory, University of Cambridge (July 1983).

    Google Scholar 

  130. L. Paulson. “Verifying the unification algorithm in LCF.” Technical report No 50, Computer Laboratory, University of Cambridge (March 1984).

    Google Scholar 

  131. L. C. Paulson. “Constructing Recursion Operators in Intuitionistic Type Theory.” Tech. Report 57, Computer Laboratory, University of Cambridge (Oct. 1984).

    Google Scholar 

  132. G.E. Peterson, M.E. Stickel. “Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms.” JACM 28,2 (1981) 233–264.

    MathSciNet  MATH  Google Scholar 

  133. T. Pietrzykowski, D.C. Jensen. “A complete mechanization of ω-order type theory.” Proceedings of ACM Annual Conference (1972).

    Google Scholar 

  134. T. Pietrzykowski. “A Complete Mechanization of Second-Order Type Theory.” JACM 20 (1973) 333–364.

    MathSciNet  MATH  Google Scholar 

  135. D. Prawitz. “Natural Deduction.” Almqist and Wiskell, Stockolm (1965).

    MATH  Google Scholar 

  136. D. Prawitz. “Ideas and results in proof theory.” Proceedings of the Second Scandinavian Logic Symposium (1971).

    Google Scholar 

  137. W. V. Quine. “The problem of simplifying truth functions.” Amer. Math. Monthly bf 59,8 (1952) 521–531.

    MathSciNet  MATH  Google Scholar 

  138. H. Rasiowa, R. Sikorski “The Mathematics of Metamathematics.” Monografie Matematyczne torn 41, PWN, Polish Scientific Publishers, Warszawa (1963).

    MATH  Google Scholar 

  139. J. C. Reynolds. “Definitional Interpreters for Higher Order Programming Languages.” Proc. ACM National Conference, Boston, (Aug. 72) 717–740.

    Google Scholar 

  140. J. C. Reynolds. “Towards a Theory of Type Structure.” Programming Symposium, Paris. Springer Verlag LNCS 19 (1974) 408–425.

    Google Scholar 

  141. J. C. Reynolds. “Types, abstraction, and parametric polymorphism.” IFIP Congress’83, Paris (Sept. 1983).

    Google Scholar 

  142. J. C. Reynolds. “Polymorphism is not set-theoretic.” International Symposium on Semantics of Data Types, Sophia-Antipolis (June 1984).

    Google Scholar 

  143. J. C. Reynolds. “Three approaches to type structure.” TAPSOFT Advanced Seminar on the Role of Semantics in Software Development, Berlin (March 1985).

    Google Scholar 

  144. J. A. Robinson. “A Machine-Oriented Logic Based on the Resolution Principle.” JACM 12 (1965) 32–41.

    Google Scholar 

  145. J. A. Robinson. “Computational Logic: the Unification Computation.” Machine Intelligence 6 Eds B. Meltzer and D.Michie, American Elsevier, New-York (1971).

    Google Scholar 

  146. K. Schütte. “Proof theory.” Springer-Verlag (1977).

    MATH  Google Scholar 

  147. D. Scott. “Constructive validity.” Symposium on Automatic Demonstration, Springer-Verlag Lecture Notes in Mathematics, 125 (1970).

    Google Scholar 

  148. 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 

  149. J.R. Shoenfield. “Mathematical Logic.” Addison-Wesley (1967).

    MATH  Google Scholar 

  150. R.E. Shostak “Deciding Combinations of Theories.” JACM 31,1 (1985) 1–12.

    MathSciNet  Google Scholar 

  151. J. Smith. “Course-of-values recursion on lists in intuitionistic type theory.” Unpublished notes, Göteborg University (Sept. 1981).

    Google Scholar 

  152. 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 

  153. R. Statman. “Intuitionistic Propositional Logic is Polynomial-space Complete.” Theoretical Computer Science 9 (1979) 67–72, North-Holland.

    MathSciNet  MATH  Google Scholar 

  154. R. Statman. “The typed Lambda-Calculus is not Elementary Recursive.” Theoretical Computer Science 9 (1979) 73–81.

    MathSciNet  MATH  Google Scholar 

  155. S. Stenlund. “Combinators λ-terms, and proof theory.” Reidel (1972).

    Google Scholar 

  156. M.E. Stickel “A Complete Unification Algorithm for Associative-Commutative Functions.” JACM 28,3 (1981) 423–434.

    MathSciNet  MATH  Google Scholar 

  157. M.E. Szabo. “Algebra of Proofs.” North-Holland (1978).

    MATH  Google Scholar 

  158. W. Tait. “A non constructive proof of Gentzen’s Hauptsatz for second order predicate logic.” Bull. Amer. Math. Soc. 72 (1966).

    Google Scholar 

  159. W. Tait. “Intensional interpretations of functionals of finite type I.” J. of Symbolic Logic 32 (1967) 198–212.

    MathSciNet  MATH  Google Scholar 

  160. W. Tait. “A Readability Interpretation of the Theory of Species.” Logic Colloquium, Ed. R. Parikh, Springer Verlag Lecture Notes 453 (1975).

    Google Scholar 

  161. M. Takahashi. “A proof of cut-elimination theorem in simple type theory.” J. Math. Soc. Japan 19 (1967).

    Google Scholar 

  162. G. Takeuti. “On a generalized logic calculus.” Japan J. Math. 23 (1953).

    Google Scholar 

  163. G. Takeuti. “Proof theory.” Studies in Logic 81 Amsterdam (1975).

    Google Scholar 

  164. R. E. Tarjan. “Efficiency of a good but non linear set union algorithm.” JACM 22,2 (1975) 215–225.

    MathSciNet  MATH  Google Scholar 

  165. R. E. Tarjan, J. van Leeuwen. “Worst-case Analysis of Set Union Algorithms.” JACM 31,2 (1985) 245–281.

    Google Scholar 

  166. A. Tarski. “A lattice-theoretical fixpoint theorem and its applications.” Pacific J. Math. 5 (1955) 285–309.

    MathSciNet  MATH  Google Scholar 

  167. 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 

  168. R. de Vrijer “Big Trees in a A-calculus with A-expressions as types.” Conference on A-calculus and Computer Science Theory, Rome, Springer-Verlag LNCS 37 (1975) 252–271.

    Google Scholar 

  169. D. Warren “Applied Logic — Its use and implementation as a programming tool.” Ph.D. Thesis, University of Edinburgh (1977).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, France

    Gérard Huet

Authors
  1. Gérard Huet
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, 8390, Passau, Federal Republic of Germany

    Manfred Broy

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huet, G. (1987). Deduction and Computation. In: Broy, M. (eds) Logic of Programming and Calculi of Discrete Design. NATO ASI Series, vol 36. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-87374-4_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-87374-4_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-87376-8

  • Online ISBN: 978-3-642-87374-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation