This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
A. Aho, J. Hopcroft, J. Ullman. “The Design and Analysis of Computer Algorithms.” Addison-Wesley (1974).
P. B. Andrews. “Resolution in Type Theory.” Journal of Symbolic Logic 36,3 (1971), 414–432.
P. B. Andrews, D. A. Miller, E. L. Cohen, F. Pfenning. “Automating higher-order logic.” Dept of Math, University Carnegie-Mellon, (Jan. 1983).
H. Barendregt. “The Lambda-Calculus: Its Syntax and Semantics.” North-Holland (1980).
E. Bishop. “Foundations of Constructive Analysis.” McGraw-Hill, New York (1967).
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.
C. Böhm, A. Berarducci. “Automatic Synthesis of Typed Lambda-Programs on Term Algebras.” Unpublished manuscript, (June 1984).
R.S. Boyer, J Moore. “The sharing of structure in theorem proving programs.” Machine Intelligence 7 (1972) Edinburgh U. Press, 101–116.
R. Boyer, J Moore. “A Lemma Driven Automatic Theorem Prover for Recursive Function Theory.” 5th International Joint Conference on Artificial Intelligence, (1977) 511–519.
R. Boyer, J Moore. “A Computational Logic.” Academic Press (1979).
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).
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).
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).
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.
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.
N.G. de Bruijn. “Automath a language for mathematics.” Les Presses de l'Université de Montréal, (1973).
N.G. de Bruijn. “Some extensions of Automath: the AUT-4 family.” Internal Automath memo M10 (Jan. 1974).
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).
M. Bruynooghe. “The Memory Management of PROLOG implementations.” Logic Programming Workshop. Ed. Tarnlund S.A (July 1980).
L. Cardelli. “ML under UNIX.” Bell Laboratories, Murray Hill, New Jersey (1982).
L. Cardelli. “Amber.” Bell Laboratories, Murray Hill, New Jersey (1985).
A. Church. “A formulation of the simple theory of types.” Journal of Symbolic Logic 5,1 (1940) 56–68.
A. Church. “The Calculi of Lambda-Conversion.” Princeton U. Press, Princeton N.J. (1941).
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).
R.L. Constable, J.L. Bates. “Proofs as Programs.” Dept. of Computer Science, Cornell University. (Feb. 1983).
R.L. Constable, J.L. Bates. “The Nearly Ultimate Pearl.” Dept. of Computer Science, Cornell University. (Dec. 1983).
Th. Coquand. “Une théorie des constructions.” Thèse de troisième cycle, Université Paris VII (Jan. 85).
Th. Coquand, G. Huet. “A Theory of Constructions.” Preliminary version, presented at the International Symposium on Semantics of Data Types, Sophia-Antipolis (June 84).
Th. Coquand, G. Huet. “Constructions: A Higher Order Proof System for Mechanizing Mathematics.” EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).
Th. Coquand, G. Huet. “Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions.” Colloque de Logique, Orsay (Juil. 1985).
Th. Coquand, G. Huet. “A Calculus of Constructions.” To appear, JCSS (1986).
J. Corbin, M. Bidoit. “A Rehabilitation of Robinson's Unification Algorithm.” IFIP 83, Elsevier Science (1983) 909–914.
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.
P.L. Curien. “Combinateurs catégoriques, algorithmes séquentiels et programmation applicative.” Thèse de Doctorat d'Etat, Université Paris VII (Dec. 1983).
P. L. Curien. “Categorical Combinatory Logic.” ICALP 85, Nafplion, Springer-Verlag LNCS 194 (1985).
P.L. Curien. “Categorical Combinators, Sequential Algorithms and Functional Programming.” Pitman (1986).
H. B. Curry, R. Feys. “Combinatory Logic Vol. I.” North-Holland, Amsterdam (1958).
D. Van Daalen. “The language theory of Automath.” Ph. D. Dissertation, Technological Univ. Eindhoven (1980).
Luis Damas, Robin Milner. “Principal type-schemas for functional programs.” Edinburgh University (1982).
P.J. Downey, R. Sethi, R. Tarjan. “Variations on the common subexpression problem.” JACM 27,4 (1980) 758–771.
Dummett. “Elements of Intuitionism.” Clarendon Press, Oxford (1977).
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).
F. Fages. “Associative-Commutative Unification.” Submitted for publication (1985).
F. Fages, G. Huet. “Unification and Matching in Equational Theories.” CAAP 83, l'Aquila, Italy. In Springer-Verlag LNCS 159 (1983).
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.
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.
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.
G. Gentzen. “The Collected Papers of Gerhard Gentzen.” Ed. E. Szabo, North-Holland, Amsterdam (1969).
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.
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).
K. Gödel. “Uber eine bisher noch nicht benutze Erweitrung des finiten Standpunktes.” Dialectica, 12 (1958).
W. D. Goldfarb. “The Undecidability of the Second-order Unification Problem.” Theoretical Computer Science, 13, (1981) 225–230.
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).
M. J. Gordon, A. J. Milner, C. P. Wadsworth. “Edinburgh LCF” Springer-Verlag LNCS 78 (1979).
W. E. Gould. “A Matching Procedure for Omega Order Logic.” Scientific Report 1, AFCRL 66-781, contract AF19 (628)-3250 (1966).
J. Guard. “Automated Logic for Semi-Automated Mathematics.” Scientific Report 1, AFCRL (1964).
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).
C. M. Hoffmann, M. J. O'Donnell. “Programming with Equations.” ACM Transactions on Programming Languages and Systems, 4,1 (1982) 83–112.
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).
G. Huet. “Constrained Resolution: a Complete Method for Type Theory.” Ph.D. Thesis, Jennings Computing Center Report 1117, Case Western Reserve University (1972).
G. Huet. “A Mechanization of Type Theory.” Proceedings, 3rd IJCAI, Stanford (Aug. 1973).
G. Huet. “The Undecidability of Unification in Third Order Logic.” Information and Control 22 (1973) 257–267.
G. Huet. “A Unification Algorithm for Typed Lambda Calculus.” Theoretical Computer Science, 1.1 (1975) 27–57.
G. Huct. “Résolution d'équations dans des langages d'ordre 1,2, ... ω.” Thèse d'Etat, Université Paris VII (1976).
G. Huet. “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems.” J. Assoc. Comp. Mach. 27,4 (1980) 797–821.
G. Huet. “A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm.” JCSS 23,1 (1981) 11–21.
G. Huet. “Initiation à la Théorie des Catégories.” Polycopié de cours de DEA, Université Paris VII (Nov. 1985).
G. Huet. “Cartesian Closed Categories and Lambda-Calculus.” Category Theory Seminar, Carnegie-Mellon University (Dec. 1985).
G. Huet, J.M. Hullot. “Proofs by Induction in Equational Theories With Constructors.” JACM 25,2 (1982) 239–266.
G. Huet, J.J. Lévy “Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems.” Rapport Laboria 359, IRIA (Aug. 1979).
G. Huet, D. Oppen. “Equations and Rewrite Rules: a Survey.” In Formal Languages: Perspectives and Open Problems, Ed. Book R., Academic Press (1980).
J.M. Hullot “Compilation de Formes Canoniques dans les Théories Equationnelles.” Thèse de 3ème cycle, U. de Paris Sud (Nov. 80).
Jean Pierre Jouannaud, Helene Kirchner. “Completion of a set of rules modulo a set of equations.” (April 1984).
L.S. Jutting. “A translation of Landau's “Grundlagen” in AUTOMATH.” Eindhoven University of Technology, Dept of Mathematics (Oct. 1976).
L.S. van Benthem Jutting. “The language theory of Λ∞, a typed λ-calculus where terms are types.” Unpublished manuscript (1984).
G. Kahn, G. Plotkin. “Domaines concrets.” Rapport Laboria 336, IRIA (Déc. 1978).
J. Ketonen, J. S. Weening. “The language of an interactive proof checker.” Stanford University (1984).
J. Ketonen. “EKL-A Mathematically Oriented Proof Checker.” 7th International Conference on Automated Deduction, Napa, California (May 1984). Springer-Verlag LNCS 170.
J. Ketonen. “A mechanical proof of Ramsey theorem.” Stanford Univ. (1983).
S.C. Kleene. “Introduction to Meta-mathematics.” North Holland (1952).
S.C. Kleene. “On the interpretation of intuitionistic number theory.” J. Symbolic Logic 31 (1945).
S.C. Kleene. “On the interpretation of intuitionistic number theory.” J. Symbolic Logic 31 (1945).
J.W. Klop. “Combinatory Reduction Systems.” Ph. D. Thesis, Mathematisch Centrum Amsterdam (1980).
D. Knuth, P. Bendix. “Simple word problems in universal algebras”. In: Computational Problems in Abstract Algebra, J. Leech Ed., Pergamon (1970) 263–297.
D.E. Knuth, J. Morris, V. Pratt. “Fast Pattern Matching in Strings.” SIAM Journal on Computing 6,2 (1977) 323–350.
G. Kreisel. “On the interpretation of nonfinitist proofs, Part I, II.” JSL 16 (1952, 1953).
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).
J. Lambek and P. J. Scott. “Aspects of Higher Order Categorical Logic.” Contemporary Mathematics 30 (1984) 145–174.
P. J. Landin. “The next 700 programming languages.” Comm. ACM 9,3 (1966) 157–166.
Philippe Le Chenadec. “Formes canoniques dans les algèbres finiment présentées.” Thèse de 3ème cycle, Univ. d'Orsay (Juin 1983).
D. Leivant. “Polymorphic type inference.” 10th ACM Conference on Principles of Programming Languages (1983).
D. Leivant. “Structural semantics for polymorphic data types.” 10th ACM Conference on Principles of Programming Languages (1983).
J.J. Lévy. “Réductions correctes et optimales dans le λ-calcul.” Thèse d'Etat, U. Paris VII (1978).
S. MacLane. “Categories for the Working Mathematician.” Springer-Verlag (1971).
D. MacQueen, G. Plotkin, R. Sethi. “An ideal model for recursive polymorphic types.” Proceedings, Principles of Programming Languages Symposium, Jan. 1984, 165–174.
D. B. MacQueen, R. Sethi. “A semantic model of types for applicative languages.” ACM Symposium on Lisp and Functional Programming (Aug. 1982).
E.G. Manes. “Algebraic Theories.” Springer-Verlag (1976).
C. Mann. “The Connection between Equivalence of Proofs and Cartesian Closed Categories.” Proc. London Math. Soc. 31 (1975) 289–310.
A. Martelli, U. Montanari. “Theorem proving with structure sharing and efficient unification.” Proc. 5th IJCAI, Boston, (1977) p 543.
A. Martelli, U. Montanari. “An Efficient Unification Algorithm.” ACM Trans. on Prog. Lang. and Syst. 4,2 (1982) 258–282.
William A. Martin. “Determining the equivalence of algebraic expressions by hash coding.” JACM 18,4 (1971) 549–558.
P. Martin-Löf. “A theory of types.” Report 71-3, Dept. of Mathematics, University of Stockholm, Feb. 1971, revised (Oct. 1971).
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).
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.
P. Martin-Löf. “Constructive Mathematics and Computer Programming.” In Logic, Methodology and Philosophy of Science 6 (1980) 153–175, North-Holland.
P. Martin-Löf. “Intuitionistic Type Theory.” Studies in Proof Theory, Bibliopolis (1984).
J. Mć Carthy. “Recursive functions of symbolic expressions and their computation by machine.” CACM 3,4 (1960) 184–195.
N. McCracken. “An investigation of a programming language with a polymorphic type structure.” Ph.D. Dissertation, Syracuse University (1979).
D.A. Miller. “Proofs in Higher-order Logic.” Ph. D. Dissertation, Carnegie-Mellon University (Aug. 1983).
D.A. Miller. “Expansion tree proofs and their conversion to natural deduction proofs.” Technical report MS-CIS-84-6, University of Pennsylvania (Feb. 1984).
R. Milner. “A Theory of Type Polymorphism in Programming.” Journal of Computer and System Sciences 17 (1978) 348–375.
R. Milner. “A proposal for Standard ML.” Report CSR-157-83, Computer Science Dept., University of Edinburgh (1983).
R.P. Nederpelt. “Strong normalization in a typed λ calculus with λ structured types.” Ph. D. Thesis, Eindhoven University of Technology (1973).
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).
G. Nelson, D.C. Oppen. “Fast decision procedures based on congruence closure.” JACM 27,2 (1980) 356–364.
M.H.A. Newman. “On Theories with a Combinatorial Definition of “Equivalence”.” Annals of Math. 43,2 (1942) 223–243.
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.
B. Nordström. “Description of a Simple Programming Language.” Report 1, Programming Methodology Group, University of Goteborg (Apr. 1984).
B. Nordström, K. Petersson. “Types and Specifications.” Information Processing 83, Ed. R. Mason, North-Holland, (1983) 915–920.
B. Nordström, J. Smith. “Propositions and Specifications of Programs in Martin-Löf's Type Theory.” BIT 24, (1984) 288–301.
A. Obtulowicz. “The Logic of Categories of Partial Functions and its Applications.” Dissertationes Mathematicae 241 (1982).
M.S. Paterson, M.N. Wegman. “Linear Unification.” J. of Computer and Systems Sciences 16 (1978) 158–167.
L. Paulson. “Recent Developments in LCF: Examples of structural induction.” Technical Report No 34, Computer Laboratory, University of Cambridge (Jan. 1983).
L. Paulson. “Tactics and Tacticals in Cambridge LCF.” Technical Report No 39, Computer Laboratory, University of Cambridge (July 1983).
L. Paulson. “Verifying the unification algorithm in LCF.” Technical report No 50, Computer Laboratory, University of Cambridge (March 1984).
L. C. Paulson. “Constructing Recursion Operators in Intuitionistic Type Theory.” Tech. Report 57, Computer Laboratory, University of Cambridge (Oct. 1984).
G.E. Peterson, M.E. Stickel. “Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms.” JACM 28,2 (1981) 233–264.
T. Pietrzykowski, D.C. Jensen. “A complete mechanization of ω-order type theory.” Proceedings of ACM Annual Conference (1972).
T. Pietrzykowski. “A Complete Mechanization of Second-Order Type Theory.” JACM 20 (1973) 333–364.
D. Prawitz. “Natural Deduction.” Almqist and Wiskell, Stockolm (1965).
D. Prawitz. “Ideas and results in proof theory.” Proceedings of the Second Scandinavian Logic Symposium (1971).
PRL staff. “Implementing Mathematics with the NUPRL Proof Development System.” Computer Science Department, Cornell University (May 1985).
H. Rasiowa, R. Sikorski “The Mathematics of Metamathematics.” Monografie Matematyczne tom 41, PWN, Polish Scientific Publishers, Warszawa (1963).
J. C. Reynolds. “Definitional Interpreters for Higher Order Programming Languages.” Proc. ACM National Conference, Boston, (Aug. 72) 717–740.
J. C. Reynolds. “Towards a Theory of Type Structure.” Programming Symposium, Paris. Springer Verlag LNCS 19 (1974) 408–425.
J. C. Reynolds. “Types, abstraction, and parametric polymorphism.” IFIP Congress'83, Paris (Sept. 1983).
J. C. Reynolds. “Polymorphism is not set-theoretic.” International Symposium on Semantics of Data Types, Sophia-Antipolis (June 1984).
J. C. Reynolds. “Three approaches to type structure.” TAPSOFT Advanced Seminar on the Role of Semantics in Software Development, Berlin (March 1985).
J. A. Robinson. “A Machine-Oriented Logic Based on the Resolution Principle.” JACM 12 (1965) 32–41.
J. A. Robinson. “Computational Logic: the Unification Computation.” Machine Intelligence 6 Eds B. Meltzer and D. Michie, American Elsevier, New-York (1971).
D. Scott. “Constructive validity.” Symposium on Automatic Demonstration, Springer-Verlag Lecture Notes in Mathematics, 125 (1970).
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).
J.R. Shoenfield. “Mathematical Logic.” Addison-Wesley (1967).
R.E. Shostak “Deciding Combinations of Theories.” JACM 31,1 (1985) 1–12.
J. Smith. “Course-of-values recursion on lists in intuitionistic type theory.” Unpublished notes, Göteborg University (Sept. 1981).
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.
R. Statman. “Intuitionistic Propositional Logic is Polynomial-space Complete.” Theoretical Computer Science 9 (1979) 67–72, North-Holland.
R. Statman. “The typed Lambda-Calculus is not Elementary Recursive.” Theoretical Computer Science 9 (1979) 73–81.
S. Stenlund. “Combinators λ-terms, and proof theory.” Reidel (1972).
M.E. Stickel “A Complete Unification Algorithm for Associative-Commutative Functions.” JACM 28,3 (1981) 423–434.
M.E. Szabo. “Algebra of Proofs.” North-Holland (1978).
W. Tait. “A non constructive proof of Gentzen's Hauptsatz for second order predicate logic.” Bull. Amer. Math. Soc. 72 (1966).
W. Tait. “Intensional interpretations of functionals of finite type I.” J. of Symbolic Logic 32 (1967) 198–212.
W. Tait. “A Realizability Interpretation of the Theory of Species.” Logic Colloquium, Ed. R. Parikh, Springer Verlag Lecture Notes 453 (1975).
M. Takahashi. “A proof of cut-elimination theorem in simple type theory.” J. Math. Soc. Japan 19 (1967).
G. Takeuti. “On a generalized logic calculus.” Japan J. Math. 23 (1953).
G. Takeuti. “Proof theory.” Studies in Logic 81 Amsterdam (1975).
R. E. Tarjan. “Efficiency of a good but non linear set union algorithm.” JACM 22,2 (1975) 215–225.
R. E. Tarjan, J. van Leeuwen. “Worst-case Analysis of Set Union Algorithms.” JACM 31,2 (1985) 245–281.
A. Tarski. “A lattice-theoretical fixpoint theorem and its applications.” Pacific J. Math. 5 (1955) 285–309.
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.
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.
D. Warren “Applied Logic — Its use and implementation as a programming tool.” Ph.D. Thesis, University of Edinburgh (1977).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Huet, G. (1986). Deduction and computation. In: Bibel, W., Jorrand, P. (eds) Fundamentals of Artificial Intelligence. Lecture Notes in Computer Science, vol 232. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022680
Download citation
DOI: https://doi.org/10.1007/BFb0022680
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16782-2
Online ISBN: 978-3-540-39875-2
eBook Packages: Springer Book Archive