Linked bibliography for the SEP article "Church's Type Theory" by Peter Andrews

This is an automatically generated and experimental page

If everything goes well, this page should display the bibliography of the aforementioned article as it appears in the Stanford Encyclopedia of Philosophy, but with links added to PhilPapers records and Google Scholar for your convenience. Some bibliographies are not going to be represented correctly or fully up to date. In general, bibliographies of recent works are going to be much better linked than bibliographies of primary literature and older works. Entries with PhilPapers records have links on their titles. A green link indicates that the item is available online at least partially.

This experiment has been authorized by the editors of the Stanford Encyclopedia of Philosophy. The original article and bibliography can be found here.

  • Andrews, P., 1963, “A Reduction of the Axioms for the Theory of Propositional Types”, Fundamenta Mathematicae, 52: 345–350. (Scholar)
  • –––, 1971, “Resolution in Type Theory”, Journal of Symbolic Logic, 36: 414–432; reprinted in Siekmann & Wrightson 1983 and in Benzmüller et al. 2008b. (Scholar)
  • –––, 1972a, “General Models and Extensionality”, Journal of Symbolic Logic, 37: 395–397; reprinted in Benzmüller et al. 2008b. (Scholar)
  • –––, 1972b, “General Models, Descriptions, and Choice in Type Theory”, Journal of Symbolic Logic, 37: 385–394 reprinted in Benzmüller et al. 2008b. (Scholar)
  • –––, 1974, “Provability in Elementary Type Theory”, Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik, 20: 411–418. (Scholar)
  • –––, 2001, “Classical Type Theory”, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Volume 2/Chapter 15, Amsterdam: Elsevier Science, pp. 965–1007. (Scholar)
  • –––, 2002, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Dordrecht: Kluwer Academic Publishers, second edition. (Scholar)
  • Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., and Xi, H., 1996, “TPS: A Theorem Proving System for Classical Type Theory”, Journal of Automated Reasoning, 16: 321–353; reprinted in Benzmüller et al. 2008b. (Scholar)
  • Andrews, P., and Brown, C., 2006, “TPS: A Hybrid Automatic-Interactive System for Developing Proofs”, Journal of Applied Logic, 4: 367–395. (Scholar)
  • Baader, F., and Snyder, W., 2001, “Unification theory”, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Volume 1/Chapter 8, Amsterdam: Elsevier Science, pp. 445–533. (Scholar)
  • Backes, J., and Brown, C., 2011, “Analytic tableaux for higher-order logic with choice”, Journal of Automated Reasoning, 47(4): 451-479. (Scholar)
  • Barendregt, H. P., 1984, The λ-Calculus, Series: Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland. (Scholar)
  • Benzmüller, C., 1999, Equality and Extensionality in Automated Higher-Order Theorem Proving, Ph.D. dissertation, Computer Science Department, Universität des Saarlandes. (Scholar)
  • Benzmüller, C., and Kohlhase, M., 1998a, “Extensional Higher-Order Resolution”, in Kirchner and Kirchner 1998, pp. 56–71. (Scholar)
  • –––, 1998b, “System Description: LEO — A Higher-Order Theorem Prover”, in Kirchner and Kirchner 1998, pp. 139–143. (Scholar)
  • Benzmüller, C., Brown, C., and Kohlhase, M., 2004, “Higher-Order Semantics and Extensionality”, Journal of Symbolic Logic, 69: 1027–1088. (Scholar)
  • –––, 2009, “Cut-simulation and impredicativity”, Logical Methods in Computer Science, 5(1:6): 1–21. (Scholar)
  • Benzmüller, C., Brown, C., Siekmann, J., and Statman, R. (eds.), 2008, Reasoning in Simple Type Theory (Festschrift in Honor of Peter B. Andrews on his 70th Birthday), King's College London: College Publications. (Scholar)
  • Benzmüller, C., Paulson, L, Theiss, F., and Fietzke, A., 2008, “LEO-II – A Cooperative Automatic Theorem Prover for Higher-Order Logic.” in A. Armando and P. Baumgartner and G. Dowek (eds.), Fourth International Joint Conference on Automated Reasoning (IJCAR'08) (Lecture Notes in Artifical Intelligence: Volume 5195), Berlin: Springer, pp. 162–170. (Scholar)
  • Brown, C., 2004, Set Comprehension in Church's Type Theory, Ph.D. dissertation, Department of Mathematical Sciences, Carnegie Mellon University. (Scholar)
  • –––, 2007, Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory (Studies in Logic: Logic and Cognitive Systems: Volume 10Z), London: College Publications. (Scholar)
  • –––, 2012, ``Satallax: An automated higher-order prover'', in 6th International Joint Conference on Automated Reasoning (IJCAR 2012), U. Sattler, B. Gramlich, and D. Miller (eds.), Dordrecht: Springer, 111–117. (Scholar)
  • Büchi, J. R., 1953, “Investigation of the Equivalence of the Axiom of Choice and Zorn's Lemma from the Viewpoint of the Hierarchy of Types”, Journal of Symbolic Logic, 18: 125–135. (Scholar)
  • Church, A., 1932, “A set of postulates for the foundation of logic (1)”, Annals of Mathematics, 33: 346–366.
  • –––, 1940, “A Formulation of the Simple Theory of Types”, Journal of Symbolic Logic, 5: 56–68; reprinted in Benzmüller et al. 2008b. (Scholar)
  • –––, 1941, The Calculi of Lambda-Conversion. Series: Annals of Mathematics Studies, Volume 6, Princeton: Princeton University Press. (Scholar)
  • –––, 1956, Introduction to Mathematical Logic, Princeton, N.J.: Princeton University Press. (Scholar)
  • Dowek, G., 2001, “Higher-Order Unification and Matching”, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning (Volume 2, Chapter 16), Amsterdam: Elsevier Science, pp. 1009–1062. (Scholar)
  • Dowek, G., and Werner, B., 2003, “Theorem Proving Modulo”, Journal of Symbolic Logic, 68: 1289–1316. (Scholar)
  • Farmer, W., 2008, “Seven Virtues of Simple Type Theory”, Journal of Applied Logic, 6: 267–286. (Scholar)
  • Gödel, K., 1931, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38: 173–198. Translated in Gödel 1986, 144–195, and in van Heijenoort 1967, 596–616. (Scholar)
  • –––, 1986, Collected Works (Volume I), Oxford: Oxford University Press. (Scholar)
  • Goldfarb, W., 1981, “The Undecidability of the Second-Order Unification Problem”, Theoretical Computer Science, 13: 225–230. (Scholar)
  • Gordon, M. J. C., 1986, “Why higher-order logic is a good formalism for specifying and verifying hardware”, in G. J. Milne and P. A. Subrahmanyam (eds.), Formal Aspects of VLSI Design, Amsterdam: North-Holland, pp. 153–177. (Scholar)
  • –––, 1988, “HOL: A Proof Generating System for Higher-Order Logic”, in G. Birtwistle and P.A. Subrahmanyam (eds.), VLSI Specification, Verification, and Synthesis, Dordrecht: Kluwer Academic Publishers, pp. 73–128. (Scholar)
  • Gordon, M.J., and Melham, T.F., 1993, Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge: Cambridge University Press. (Scholar)
  • Gould, W. E., 1966, A Matching Procedure for ω-order Logic, Ph.D. dissertation, Mathematics Department, Princeton University. (Scholar)
  • Henkin, L., 1950, “Completeness in the Theory of Types”, Journal of Symbolic Logic, 15: 81–91; reprinted in Hintikka 1969 and in Benzmüller et al. 2008b. (Scholar)
  • –––, 1963, “A Theory of Propositional Types”, Fundamenta Mathematicae, 52: 323–344. (Scholar)
  • –––, 1975, “Identity as a logical primitive”, Philosophia, 5(1–2): 31–45. (Scholar)
  • Hilbert, D., 1928, “Die Grundlagen der Mathematik”, Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universität, 6: 65–85; translated in van Heijenoort 1967, pp. 464–479. (Scholar)
  • Hintikka, J. (ed.), 1969, The Philosophy of Mathematics, Oxford: Oxford University Press. (Scholar)
  • Huet, G. P., 1973a, “A Mechanization of Type Theory”, in Proceedings of the Third International Joint Conference on Artificial Intelligence (Stanford University), Los Altos, CA: William Kaufman, pp. 139–146. (Scholar)
  • –––, 1973b, “The Undecidability of Unification in Third-order Logic”, Information and Control, 22: 257–267. (Scholar)
  • –––, 1975, “A Unification Algorithm for Typed λ-Calculus”, Theoretical Computer Science, 1: 27–57. (Scholar)
  • Jensen, D. C., Pietrzykowski, T., 1976, “Mechanizing ω-Order Type Theory Through Unification”, Theoretical Computer Science, 3: 123–171. (Scholar)
  • Kirchner, C., and Kirchner, H. (eds.), 1998, Proceedings of the 15th International Conference on Automated Deduction, Series: Lecture Notes in Artificial Intelligence, Volume 1421, London: Springer-Verlag. (Scholar)
  • Kohlhase, M., 1993, “A Unifying Principle for Extensional Higher-Order Logic”, Technical Report 93–153, Department of Mathematics, Carnegie Mellon University. (Scholar)
  • –––, 1995, “Higher-Order Tableaux”, in P. Baumgartner, R. Hähnle, and J. Posegga (eds.), Theorem Proving with Analytic Tableaux and Related Methods (4th International Workshop, TABLEAUX '95, Schloß; Rheinfels, St. Goar, Germany, May 1995), Series: Lecture Notes in Artificial Intelligence, Volume 918, Berlin: Springer-Verlag. (Scholar)
  • –––, 1998, “Higher-Order Automated Theorem Proving”, in Wolfgang Bibel and Peter Schmitt (eds.), Automated Deduction — A Basis for Applications, Volume 1, Dordrecht: Kluwer, pp. 431–462. (Scholar)
  • Konrad, K., 1998, “HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux”, in J. Grundy and M. Newey (eds.), Theorem Proving in Higher Order Logics (11th International Conference, TPHOLs'98, Canberra, Australia), Series: Lecture Notes in Computer Science, Volume 1479, Berlin: Springer-Verlag, pp. 245–261. (Scholar)
  • Maslov, S. Ju., 1967, “An Inverse Method for Establishing Deducibility of Nonprenex Formulas of Predicate Calculus”, Soviet Mathematics Doklady, 8: 16–19. (Scholar)
  • Miller, D. A., 1983, Proofs in Higher-Order Logic, Ph.D. dissertation, Mathematics Department, Carnegie Mellon University. (Scholar)
  • –––, 1987, “A Compact Representation of Proofs”, Studia Logica, 46/4: 347–370. (Scholar)
  • Mints, G., 1999, “Cut-elimination for simple type theory with an axiom of choice”, Journal of Symbolic Logic, 64: 479–485. (Scholar)
  • Montague, Richard, 1974, Formal Philosophy. Selected Papers Of Richard Montague, edited and with an introduction by Richmond H. Thomason, New Haven: Yale University Press. (Scholar)
  • Muskens, R., 2007, “Intensional Models for the Theory of Types”, Journal of Symbolic Logic, 72: 98–118. (Scholar)
  • Nipkow, T., Paulson, L., and Wenzel, M., 2002, Isabelle/HOL – A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science: Vol. 2283), Berlin: Springer. (Scholar)
  • Owre, S., Rajan, S., Rushby, J.M., Shankar, N., and Srivas, M., 1996, “PVS: Combining Specification, Proof Checking, and Model Checking”, in R. Alur and T. A. Henzinger (eds.), Computer-Aided Verification, Series: Lecture Notes in Computer Science, Volume 1102, Berlin: Springer-Verlag, pp. 411–414. (Scholar)
  • Prawitz, D., 1968, “Hauptsatz for Higher Order Logic”, Journal of Symbolic Logic, 33: 452–457. (Scholar)
  • Quine, W., 1956, “Unification of universes in set theory” (abstract), Journal of Symbolic Logic, 21: 216. (Scholar)
  • Russell, B., 1903, The Principles of Mathematics, Cambridge: Cambridge University Press. (Scholar)
  • –––, 1908, “Mathematical Logic as Based on the Theory of Types”, American Journal of Mathematics, 30: 222–262; reprinted in van Heijenoort 1967, pp. 150–182. (Scholar)
  • Schönfinkel, M., 1924, “Über die Bausteine der mathematischen Logik”, Mathematische Annalen, 92: 305–316; translated in van Heijenoort 1967, pp. 355–366. (Scholar)
  • Shankar, N., 2001, “Using Decision Procedures with a Higher-Order Logic”, in R. J. Boulton and P. B. Jackson (eds.), Theorem Proving in Higher Order Logics (14th international conference, TPHOLs 2001, Edinburgh, Scotland), Series: Lecture Notes in Computer Science, Volume 2152, Berlin: Springer-Verlag, pp. 5–26. (Scholar)
  • Siekmann, J., and Wrightson, G. (eds.), 1983, Automation of Reasoning (Classical Papers on Computational Logic 1967–1970: Vol. 2), Berlin: Springer-Verlag. (Scholar)
  • Smullyan, R. M., 1963, “A Unifying Principle in Quantification Theory”, Proceedings of the National Academy of Sciences (U.S.A.), 49: 828–832. (Scholar)
  • –––, 1995, First-Order Logic, New York: Dover, second corrected edition. (Scholar)
  • Stenlund, S., 1972, λ-terms and Proof Theory, Dordrecht: D. Reidel. (Scholar)
  • Takahashi, M., 1967, “A Proof of Cut-Elimination Theorem in Simple Type Theory”, Journal of the Mathematical Society of Japan, 19: 399–410. (Scholar)
  • –––, 1970, “A System of Simple Type Theory of Gentzen Style with Inference on Extensionality, and the Cut Elimination in it”, Commentarii Mathematici Universitatis Sancti Pauli, 18: 129–147. (Scholar)
  • Tarski, A., 1923, “Sur le terme primitif de la Logistique”, Fundamenta Mathematicae, 4: 196–200; translated in Tarski 1956, 1–23. (Scholar)
  • –––, 1956, Logic, Semantics, Metamathematics, Oxford: Oxford University Press. (Scholar)
  • van Heijenoort, J., 1967, From Frege to Gödel. A Source Book in Mathematical Logic 1879–1931, Cambridge, MA: Harvard University Press. (Scholar)
  • Whitehead, A. N., and Russell, B., 1927a, Principia Mathematica, Volume 1, Cambridge: Cambridge University Press, second edition. (Scholar)
  • –––, 1927b, “Incomplete Symbols”, in Whitehead & Russell 1927a, 66–84; reprinted in van Heijenoort 1967, 216–223. (Scholar)
  • Yasuhara, M., 1975, “The Axiom of Choice in Church's Type Theory” (abstract), Notices of the American Mathematical Society, 22 (January): A34. (Scholar)

Generated Sun Jun 17 10:55:07 2018