William M. Farmer

Professor
Department of Computing and Software
McMaster University

Publications (and some selected technical reports and tutorials)

A. MathScheme Project

  1. High-level theories Abstract PostScript PDF Online
    J. Carette and W. M. Farmer
    In: S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk, eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 5144:232–245, 2008.
  2. Biform theories in Chiron Abstract PostScript PDF Online
    W. M. Farmer
    In: M. Kauers, M. Kerber, R. R. Miner, and W. Windsteiger, eds., Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science (LNCS), 4573:66–79, 2007.
  3. A rational reconstruction of a system for experimental mathematics Abstract PostScript PDF Online
    J. Carette, W. M. Farmer, and V. Sorge
    In: M. Kauers, M. Kerber, R. R. Miner, and W. Windsteiger, eds., Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science (LNCS), 4573:13–26, 2007.
  4. A rational reconstruction of a system for experimental mathematics
    J. Carette, W. M. Farmer, and V. Sorge
    In: S. Colton, ed., Proceedings of the Fourteenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, Imperial College, London, UK, April 19--20, 2007.
    Abstract.
  5. Trustable communication between mathematics systems Abstract PostScript PDF
    J. Carette, W. M. Farmer, and J. Wajs
    SQRL Report No. 41, 22 pp., McMaster University, 2004.
    This is a longer, revised version of the paper below with the same name.
  6. Trustable communication between mathematics systems Abstract PostScript PDF
    J. Carette, W. M. Farmer, and J. Wajs
    In: T. Hardin and R. Rioboo, eds., Calculemus 2003 (11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Rome, Italy, September 2003), pp. 58–68, Aracne, Rome, Italy, 2003.
    This is a shorter, preliminary version of the paper above with the same name.
  7. An overview of a Formal Framework for Managing Mathematics Abstract PostScript PDF
    W. M. Farmer and M. v. Mohrenschildt
    In: B. Buchberger, G. Gonnet, and M. Hazewinkel, eds, Mathematical Knowledge Management, special issue of Annals of Mathematics and Artificial Intelligence, 38:165–191, 2003.
  8. A Formal Framework for Managing Mathematics Online
    W. M. Farmer and M. v. Mohrenschildt
    In: B. Buchberger and O. Caprotti, eds, Electronic Proceedings of the First International Workshop on Mathematical Knowledge Management: MKM 2001, 37 pp., RISC, Hagenburg, Austria, September 24–26, 2001.
    Preliminary version of the paper above.
  9. A proposal for the development of an interactive mathematics laboratory for mathematics education PostScript PDF
    W. M. Farmer
    In: E. Melis, ed., Proceedings of the Workshop on Deduction Systems for Mathematics Education, pp. 20–25, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 16, 2000.
  10. Transformers for symbolic computation and formal deduction Abstract PostScript PDF
    W. M. Farmer and M. v. Mohrenschildt
    In: S. Colton, U. Martin and V. Sorge, eds., Proceedings of the Workshop on the Role of Automated Deduction in Mathematics, pp. 36–45, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 20–21, 2000.
  11. The Interactive Mathematics Laboratory Abstract Online
    W. M. Farmer
    In: Proceedings of the 31st Annual Midwest Instruction and Computing Symposium (MICS '98), pp. 84–94, Fargo, North Dakota and Moorhead, Minnesota, April 16–18, 1998.

B. IMPS Interactive Mathematical Proof System

  1. Panoptes: An exploration tool for formal proofs Abstract PDF
    W. M. Farmer and O. Grigorov
    In: S. Autexier and C. Benzmüller, eds., Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers (UITP'08) (TPHOLs 2008, Concordia University, Montréal, Québec, Canada, August 22, 2008), Electronic Notes in Theoretical Computer Science (ENTCS), 226:39--48, 2009.
    DOI: 10.1016/j.entcs.2008.12.096.
  2. IMPS Abstract
    W. M. Farmer
    In: F. Wiedijk, ed., The Seventeen Provers of the World, Lecture Notes in Computer Science (LNCS), 3600:72–87, 2006.
  3. A scheme for defining partial higher-order functions by recursion Abstract PostScript PDF Online
    W. M. Farmer
    In: A. Butterfield, ed., 3rd Irish Workshop on Formal Methods, 13 pp., electronic Workshops in Computing, Springer-Verlag, 1999.
  4. IMPS: An updated system description PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer Fábrega
    In: M. McRobbie and J. Slaney, eds., Automated Deduction—CADE-13, Lecture Notes in Computer Science (LNCS), 1104:298–302, 1996.
  5. Contexts in mathematical reasoning and computation Abstract
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Symbolic Computation, 19:201–216, 1995.
  6. Proof script pragmatics in IMPS Abstract PostScript PDF
    W. M. Farmer, J. D. Guttman, M. E. Nadel, and F. J. Thayer
    In: A. Bundy, ed., Automated Deduction—CADE-12, Lecture Notes in Computer Science (LNCS), 814:356–370, 1994.
  7. Reasoning with contexts
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: A. Miola, ed., Design and Implementation of Symbolic Computation Systems, Lecture Notes in Computer Science (LNCS), 722:216–228, 1993.
    Preliminary version of Contexts in mathematical reasoning and computation.
  8. The IMPS user's manual HTML PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Technical Report M-93B138, 289 pp., The MITRE Corporation, November 1993.
  9. IMPS: An Interactive Mathematical Proof System Abstract PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Automated Reasoning, 11:213–248, 1993.
  10. IMPS: System description PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: D. Kapur, ed., Automated Deduction—CADE-11, Lecture Notes in Computer Science (LNCS), 607:701–705, 1992.
  11. Two computer-supported proofs in metric space topology PostScript PDF
    W. M. Farmer and F. J. Thayer
    Notices of the American Mathematical Society, 38:1133–1138, 1991.
  12. IMPS: An Interactive Mathematical Proof System (system description)
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: M. E. Stickel, ed., 10th International Conference on Automated Deduction, Lecture Notes in Computer Science (LNCS), 449:653–654, 1990.
    Abstract.

C. Logics and Set Theories for Mechanized Mathematics

  1. Logics with undefinedness PDF
    W. M. Farmer
    Tutorial given at CADE-22, McGill University, Montreal, Quebec, Canada, August 2, 2009.
  2. Andrews' type system with undefinedness Abstract PostScript PDF
    W. M. Farmer
    In: C. Benzmueller, C. Brown J. Siekmann, and R. Statman, eds., Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday, Studies in Logic, pp. 223–242, College Publications, 2008.
  3. The seven virtues of simple type theory Abstract PostScript PDF Online
    W. M. Farmer
    Journal of Applied Logic, 6:267–286, 2008.
    DOI: 10.1016/j.jal.2007.11.001.
  4. Chiron: A set theory with types, undefinedness, quotation, and evaluation Abstract PostScript PDF
    W. M. Farmer
    SQRL Report No. 38, 121 pp., McMaster University, 2007 (revised 2009).
  5. Chiron: A multi-paradigm logic Abstract PostScript PDF
    W. M. Farmer
    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.
  6. Formalizing undefinedness arising in calculus Abstract PostScript PDF Online
    W. M. Farmer
    In: D. Basin and M. Rusinowitch, eds., Automated Reasoning, Lecture Notes in Computer Science (LNCS), 3097:475–489, 2004.
  7. A basic extended simple type theory Abstract PostScript PDF
    W. M. Farmer
    SQRL Report No. 14, 12 pp., McMaster University, 2003 (revised 2004).
  8. STMM: A Set Theory for Mechanized Mathematics Abstract PostScript PDF
    W. M. Farmer
    Journal of Automated Reasoning, 26:269–289, 2001.
  9. A set theory with support for partial functions Abstract PostScript PDF
    W. M. Farmer and J. D. Guttman
    In: E. Thijsse, F. Lepage, and H. Wansing, eds, Partiality and Modality, special issue of Studia Logica, 66:59–78, 2000.
  10. STMM and partial functions
    W. M. Farmer
    In: M. Kerber, ed., Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 3–14, CADE-15, Lindau, Germany, July 5, 1998.
    Preliminary version of STMM: A Set Theory for Mechanized Mathematics.
  11. A set theory for mechanized mathematics
    W. M. Farmer
    926th AMS Meeting Program (Southeast Sectional Meeting, Georgia Institute of Technology), p. 481, American Mathematical Society, October 17–19, 1997.
    Abstract.
  12. Mechanizing the traditional approach to partial functions Abstract PostScript PDF
    W. M. Farmer
    In: W. Farmer, M. Kerber, and M. Kohlhase, eds., Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 27–32, CADE-13, Rutgers University, New Brunswick, New Jersey, July 30, 1996.
    Abbreviated version of Reasoning about partial functions with the aid of a computer.
  13. Reasoning about partial functions with the aid of a computer Abstract
    W. M. Farmer
    Erkenntnis, 43:279–294, 1995.
  14. A simple type theory with partial functions and subtypes Abstract
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211–240, 1993.
  15. A simple theory of types with partial functions and subtypes
    W. M. Farmer and J. D. Guttman
    Journal of Symbolic Logic 58:754, 1993.
    Abstract.
  16. A partial functions version of Church's simple theory of types Abstract
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269–1291, 1990.

D. Mathematical Knowledge Management (MKM)

  1. A review of Mathematical Knowledge Management Abstract PDF
    J. Carette and W. M. Farmer
    In: J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt, eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 5625:233–246, 2009.
  2. Mathematical knowledge management Abstract
    W. M. Farmer
    In: D. G. Schwartz, ed., Encyclopedia of Knowledge Management, pp. 599–604, Information Science Reference, 2005. Online
    Also in: M. E. Jennex, ed., Knowledge Management: Concepts, Methodologies, Tools and Applications, Chapter 7.3, pp. 2976–2983, Information Science Reference, 2007. Online
  3. MKM: A new interdisciplinary field of research Abstract PostScript PDF
    W. M. Farmer
    ACM SIGSAM Bulletin, 38:47–52, 2004.

E. Little Theories Method

  1. An infrastructure for intertheory reasoning Abstract PostScript PDF Online
    W. M. Farmer
    In: D. McAllester, ed., Automated Deduction—CADE-17, Lecture Notes in Computer Science (LNCS), 1831:115–131, 2000.
  2. Perspective switching using theories and interpretations PostScript PDF
    W. M. Farmer
    In: J. Albus, A. Meystel, and R. Quintero, eds., Intelligent Systems: A Semiotic Perspective, Vol. I, pp. 206–207, National Institute of Standards and Technology, Gaithersburg, MD, October 20–23, 1996.
    Abstract.
  3. Theory interpretation in simple type theory Abstract PostScript PDF
    W. M. Farmer
    In: J. Heering et al., eds., Higher-Order Algebra, Logic, and Term Rewriting, Lecture Notes in Computer Science (LNCS), 816:96–123, 1994.
  4. A general method for safely overwriting theories in mechanized mathematics systems Abstract PostScript PDF
    W. M. Farmer
    Technical Report, 21 pp., The MITRE Corporation, 1994.
  5. A general method for safely overwriting theories in mechanized mathematics systems
    W. M. Farmer
    In: D. Basin, F. Giunchiglia, and M. Kaufmann, eds., Proceedings of the Workshop on the Correctness and Metatheoretical Extensibility of Automated Reasoning Systems, pp. 46–48, CADE-12, Nancy, France, June 26, 1994.
    Abstract.
  6. Little theories Abstract PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: D. Kapur, ed., Automated Deduction—CADE-11, Lecture Notes in Computer Science (LNCS), 607:567–581, 1992.
  7. Theory interpretations in computerized mathematics
    W. M. Farmer
    Journal of Symbolic Logic, 57:356, 1992.
    Abstract.
  8. Abstract data types in many-sorted second-order logic
    W. M. Farmer
    Technical Report M87-64, 29 pp., The MITRE Corporation, October 1987.

F. Formal Methods

  1. A verified compiler for Multithreaded PreScheme Abstract Online
    W. M. Farmer and J. D. Ramsdell
    Technical Report, 180 pp., The MITRE Corporation, 1996.
  2. Formal numerical program analysis Abstract PostScript PDF
    W. M. Farmer and F. J. Thayer
    Technical Report, 52 pp., The MITRE Corporation, 1994.
  3. 8 papers on the VLISP verified programming language implementation Online
    W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell, and V. Swarup
    Technical Reports M-92B91, ..., M-92B98, 487 pp., The MITRE Corporation, September 1992.
  4. Towards a discipline for developing verified software Abstract
    W. M. Farmer, D. M. Johnson, and F. J. Thayer
    In: J. H. Burrows and P. R. Gallagher, Jr., eds., Proceedings of the 9th National Computer Security Conference, pp. 91–98, National Bureau of Standards, Gaithersburg, Maryland, September 15–18, 1986.
    Also in: R. Turn, ed., Advances in Computer System Security, Vol. III, Artech House, Norwood, Massachusetts, pp. 176–183, 1988.

G. Security of Mobile Agents

  1. Security for mobile agents: Issues and requirements Abstract PostScript PDF
    W. M. Farmer, J. D. Guttman, and V. Swarup
    In: S. Wakid and J. Davis, eds., Proceedings of the 19th National Information Systems Security Conference, Vol. 2, pp. 591–597, Baltimore Convention Center, Baltimore, Maryland, October 22–25, 1996.
  2. Security for mobile agents: Authentication and state appraisal Abstract PostScript PDF
    W. M. Farmer, J. D. Guttman, and V. Swarup
    In: E. Bertino et al., eds., Computer Security—ESORICS 96, Lecture Notes in Computer Science (LNCS), 1146:118–130, 1996.

H. Graph Rewriting and Combinatory Algebra

  1. Redex capturing in term graph rewriting (concise version)
    W. M. Farmer and R. J. Watro
    In: R. V. Book, ed., Rewriting Techniques and Applications, Lecture Notes in Computer Science (LNCS), 488:13–24, 1991.
  2. Redex capturing in term graph rewriting Abstract
    W. M. Farmer and R. J. Watro
    International Journal of the Foundations of Computer Science, 1:369–386, 1990.
  3. A correctness proof for combinator reduction with cycles Abstract
    W. M. Farmer, J. D. Ramsdell, and R. J. Watro
    ACM Transactions on Programming Languages and Systems, 12:123–134, 1990.
  4. A correctness proof for combinator reduction with cycles
    W. M. Farmer, J. D. Ramsdell, and R. J. Watro
    Journal of Symbolic Logic, 55:373–374, 1990.
    Abstract.
  5. Computing with the Curry Chip Abstract
    W. M. Farmer, J. D. Ramsdell, and R. J. Watro
    Technical Report M89-59, 89 pp., The MITRE Corporation, September 1989.

I. Higher-Order Unification

  1. Simple second-order languages for which unification is undecidable Abstract
    W. M. Farmer
    Theoretical Computer Science, 87:25–41, 1991.
  2. A unification algorithm for second-order monadic terms Abstract
    W. M. Farmer
    Annals of Pure and Applied Logic, 39:131–174, 1988.
  3. An algorithm for the unification of second-order monadic terms
    W. M. Farmer
    Journal of Symbolic Logic, 51:841–842, 1986.
    Abstract.

J. Length of Proofs

  1. The Kreisel length-of-proof problem Abstract
    W. M. Farmer
    In: Logic and Combinatorics, eds. J. Franco, J. M. Dunn, and W. H. Wheeler, special issue of Annals of Mathematics and Artificial Intelligence, 6:27–55, 1992.
  2. A unification-theoretic method for investigating the k-provability problem Abstract
    W. M. Farmer
    Annals of Pure and Applied Logic, 51:173–214, 1991.
  3. The k-provability problem for Gentzen-style sequent systems Abstract
    W. M. Farmer
    Technical Report M89-20, 13 pp., The MITRE Corporation, February 1989.
  4. Some results on the k-provability problem
    W. M. Farmer
    Journal of Symbolic Logic, 53:1003, 1988.
    Abstract.
  5. Length of Proofs and Unification Theory Abstract
    W. M. Farmer
    Ph.D. Thesis, University of Wisconsin-Madison, 1984.

K. Education

  1. The use of formal reasoning technology in mathematics education: Opportunities and challenges Abstract
    W. M. Farmer
    In: P. Courtieu and H. Geuvers, eds., Proceedings of the Workshop on Proof Assistants and Types in Education (PATE 2007), Paris, France, June 25, 2007.
    Abstract.
  2. Simple type theory: Simple steps towards a formal specification Abstract Online
    W. M. Farmer and M. v. Mohrenschildt
    In: Proceedings of the 34th Annual Frontiers in Education (FIE 2004), CD-ROM, IEEE, pp. F1C-1–F1C-6, 2004.
  3. Network instructional units Online
    W. M. Farmer and R. E. Mowe
    In: Proceedings of the 32st Annual Midwest Instruction and Computing Symposium (MICS '99), 9 pp., La Crosse, Wisconsin, April 15–17, 1999.

L. Miscellaneous

  1. A simple framework for contracts in federated database systems Abstract PostScript PDF
    W. M. Farmer and M. E. Nadel
    Technical Report, 22 pp., The MITRE Corporation, 1995.

M. Edited Conference Proceedings

  1. Mathematical Knowledge Management (5th International Conference, MKM 2006, Wokingham, UK, August 2006, Proceedings) Online
    J. M. Borwein and W. M. Farmer, eds.
    Lecture Notes in Computer Science (LNCS), 4108:1–295, 2006.
  2. Proceeding of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005) Online
    J. Carette and W. M. Farmer, eds.
    Electronic Notes in Theoretical Computer Science (ENTCS), 151:1–178, 2006.
  3. Proceedings of the Workshop on the Mechanization of Partial Functions Online
    W. Farmer, M. Kerber, and M. Kohlhase, eds.
    CADE-13, Rutgers University, New Brunswick, New Jersey, USA, July 30, 1996.

N. Reviews

  1. Review of Jan Krajícek, On the number of steps in proofs, Annals of Pure and Applied Logic, 41:153–178, 1989.
    W. M. Farmer, Journal of Symbolic Logic, 56:334–335, 1991.
  2. Review of Jan Krajícek, The number of proof lines and the size of proofs in first order logic, Archive for Mathematical Logic, 27:69–84, 1988.
    W. M. Farmer, Journal of Symbolic Logic, 54:1107–1108, 1989.
  3. Review of Larry Wos, Automated Reasoning: 33 Basic Research Problems, Prentice Hall, Englewood Cliffs, New Jersey, 1988.
    W. M. Farmer, Journal of Symbolic Logic, 53:1258–1259, 1988.