Computing and Software 734
Formalized Mathematics
Winter 2014

Instructor: William M. Farmer

References

01 What is Formalized Mathematics?

  1. A. Doxiadis and C. Papadimitriou, Logicomix, Bloomsbury Publishing, 2009.
  2. H. Geuvers, Proof assistants: History, ideas, and future, Sadhana 34:3–25, 2009. Online.
  3. I. Lakatos, Proofs and Refutations, Cambridge University Press, 1976.
  4. Biographical Sketch of Imre Lakatos.
  5. A. N. Whitehead and B. Russell, Principia Mathematica, Cambridge University Press, 1910–1913.

02 Review of Mathematical Logic

03 Review of First-Order Logic

  1. R. M. Smullyan, First-Order Logic, Dover, 1995.

04 Simple Type Theory

  1. P. B. Andrews, "A Reduction of the Axioms for the Theory of Propositional Types", Fundamenta Mathematicae, 52:345–350, 1963.
  2. P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Kluwer, 2002.
  3. P. B. Andrews, "Church's Type Theory", in: E. N. Zalta, ed., The Stanford Encyclopedia of Philosophy, Spring 2009. Article
  4. B. Russell, "Mathematical Logic as Based on the Theory of types", American Journal of Mathematics, 30:222–262, 1908.
  5. A. Church, "A formulation of the simple theory of types", Journal of Symbolic Logic, 5:56–68, 1940.
  6. W. M. Farmer, "A basic extended simple type theory", SQRL Report No. 14, 12 pp., McMaster University, 2003 (revised 2004). PDF
  7. W. M. Farmer, "The seven virtues of simple type theory", Journal of Applied Logic, 6:267–286, 2008. PDF
  8. L. Henkin, "Completeness in the Theory of Types", Journal of Symbolic Logic, 15:81–91, 1950.
  9. L. Henkin, "A Theory of Propositional Types", Fundamenta Mathematicae, 52:323–344, 1963.

05 Other Interactive Theorem Proving Systems

  1. F. Wiedijk, "Comparing mathematical provers", in: A. Asperti, B. Buchberger, and J. Davenport, eds., Mathematical Knowledge Management, LNCS, 2594:188–202, 2003. PostScript PDF

06 Practise-Oriented Logics

  1. W. M. Farmer, "A partial functions version of Church's simple theory of types", Journal of Symbolic Logic, 55:1269–1291, 1990.
  2. W. M. Farmer, "Reasoning about partial functions with the aid of a computer", Erkenntnis, 43:279–294, 1995.
  3. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59–78, 2000. PostScript PDF
  4. W. M. Farmer, "STMM: A Set Theory for Mechanized Mathematics", Journal of Automated Reasoning, 26:269–289, 2001. PostScript PDF
  5. W. M. Farmer, "Formalizing undefinedness arising in calculus", in: D. Basin and M. Rusinowitch, eds., Automated Reasoning, LNCS, 3097:475–489, 2004. PostScript PDF
  6. W. M. Farmer, "Chiron: A multi-paradigm logic", in: R. Matuszewski and A. Zalewska, eds, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, 10(23):1–19, 2007. PostScript PDF
  7. W. M. Farmer, "Logics with Undefinedness: How to Modify a Traditional Logic so that It handles Undefinedness in Accordance with Mathematical Practice", a half-day tutorial at the 22nd International Conference on Automated Deduction (CADE-22), McGill University, Montreal, Quebec, Canada, August 2–7, 2009. PDF

07 The Little Theories Method

  1. J. Barwise and J. Seligman, Information Flow : The Logic of Distributed Systems, Cambridge University Press, 1997.
  2. R. Burstall and J. Goguen, "Putting theories together to make specifications", Proceedings of the Fifth International Joint Conference on Artificial Intelligence, pp. 1045–1058, 1977.
  3. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "Little theories", in: D. Kapur, ed., Automated Deduction--CADE-11, LNCS, 607:567–581, 1992. PostScript PDF
  4. W. M. Farmer, "Theory interpretation in simple type theory", in: J. Heering et al., eds., Higher-Order Algebra, Logic, and Term Rewriting, LNCS, 816:96–123, 1994. PostScript PDF
  5. W. M. Farmer, "An infrastructure for intertheory reasoning", in: In: D. McAllester, ed., Automated Deduction--CADE-17, LNCS, 1831:115–131, 2000. PostScript PDF
  6. J. Carette, W. M. Farmer, and J. Wajs, "Trustable communication between mathematics systems", Technical Report, 22 pp., McMaster University, 2004. (This is a longer, revised version of the paper with the same name published in the proceedings of Calculemus 2003.) PostScript PDF
  7. R. Nakajima and T. Yuasa (eds.), The IOTA Programming System, LNCS, Vol. 160, 1982.
  8. D. Sannella and A. Tarlecki, "Towards formal development of programs from algebraic specifications: Implementations revisited", Acta Informatica, 25:233–281, 1988.
  9. D. Smith and M. Lowry, "Algorithmic theories and design tactics", Science of Computer Programming, 14:305–321, 1990
  10. W. Turski and T. Maibaum, The Specification of Computer Programs, Addison-Wesley, 1987.