William M. Farmer

Professor
Department of Computing and Software
McMaster University

Publications

Table of Contents

  1. Formal Mathematics for the Masses Project
  2. MathScheme Project
  3. Tetrapod Project
  4. IMPS Interactive Mathematical Proof System
  5. Simple Type Theory
  6. Set Theories for Mechanized Mathematics
  7. Undefinedness and Partial Functions
  8. Logics with Quotation and Evaluation
  9. Little Theories Method
  10. Mathematical Knowledge Management (MKM)
  11. Formal Methods
  12. Security of Mobile Agents
  13. Graph Rewriting and Combinatory Algebra
  14. Higher-Order Unification
  15. Length of Proofs
  16. Education
  17. Miscellaneous
  18. Edited Conference Proceedings
  19. Reviews

Notes

  1. The entries below include some selected unpublished technical reports and tutorials.
  2. Several entries appear under more than one topic.
  3. The 10 publications that are most important in my judgment are written in red, and the 21 that are next most important are written in green.

A. Formal Mathematics for the Masses Project

  1. Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas Springer Link Corrigenda
    W. M. Farmer
    309 pp., Computer Science Foundations and Applied Logic, Birkhäuser/Springer, 2023.
  2. Monoid theory in Alonzo: A little theories formalization in simple type theory Abstract PDF
    W. M. Farmer
    arXiv:2312.05658 (76 pp.), 2023.
  3. LaTeX for Alonzo Abstract PDF
    W. M. Farmer
    60 pp., 2023 (revised 2024).
  4. Formal mathematics for the masses Abstract PDF CEUR Workshop Proceedings
    W. M. Farmer
    In: J. Blanchette, J, Davenport, P. Koepke, M. Kohlhase, A. Kohlhase, A. Naumowicz, D. Müller, Y. Sharoda, and C. Sacerdoti Coen, eds., Workshop Papers at 14th Conference on Intelligent Computer Mathematics (CICM 2021), CEUR Workshop Proceedings, Vol. 3377, 8 pp., CEUR-WS.org, 2023.

B. MathScheme Project

  1. Leveraging the information contained in theory presentations Abstract PDF Springer Link
    J. Carette, W. M. Farmer, Y. Sharoda
    In: C. Benzmüller and B. Miller, eds., Intelligent Computer Mathematics (CICM 2020), Lecture Notes in Computer Science (LNCS), 12236:55–70, 2020.
    Preprint: arXiv:2006.09292, 2020.
  2. Towards specifying symbolic computation Abstract PDF Springer Link
    J. Carette and W. M. Farmer
    In: C. Kalisyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen, eds., Intelligent Computer Mathematics (CICM 2019), Lecture Notes in Computer Science (LNCS), 11617:109–124, 2019.
    Preprint: arXiv:1904.02729, 2019.
  3. Biform Theories: Project description Abstract PDF Springer Link
    J. Carette, W. M. Farmer, and Y. Sharoda
    In: F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef, eds., Intelligent Computer Mathematics (CICM 2018), Lecture Notes in Computer Science (LNCS), 11006:76–86, 2018.
    Preprint: arXiv:1805.02709, 2018.
  4. HOL Light QE Abstract PDF Springer Link
    J. Carette, W. M. Farmer, and P. Laskowski
    In: J. Avigad and A. Mahboubi, eds., Interactive Theorem Proving (ITP 2018), Lecture Notes in Computer Science (LNCS), 10895:215–234, 2018.
    Preprint: arXiv:1802.00405, 2018.
  5. Formalizing mathematical knowledge as a biform theory graph: A case study Abstract PDF Springer Link
    J. Carette and W. M. Farmer
    In: H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science (LNCS), 10383:9–24, 2017 (without appendices).
    Preprint with appendices: arXiv:1704.02253 (43 pp.), 2017.
  6. Meaning formulas for syntax-based mathematical algorithms PDF
    W. M. Farmer
    In: T. Kutsia and A. Voronkov, eds., SCSS 2014 (6th International Symposium on Symbolic Computation in Software Science), EasyChair Proceedings in Computing (EPiC), 30:10–11, 2014.
    Extended Abstract.
  7. Mechanising mathematics (text interview) PDF
    In: International Innovation North America, May 2013, pp. 20–22, Research Media, 2013.
  8. The formalization of syntax-based mathematical algorithms using quotation and evaluation Abstract PDF Springer Link
    W. M. Farmer
    In: J. Carette et al., eds., Intelligent Computer Mathematics (CICM 2013), Lecture Notes in Computer Science (LNCS), 7961:35–50, 2013.
    Preprint: arXiv:1305.6052, 2013.
  9. Frameworks for reasoning about syntax that utilize quotation and evaluation Abstract PDF
    W. M. Farmer and P. Larjani
    McSCert Report 9, 38 pp., McMaster University, 2013 (revised 2014).
    Preprint: arXiv:1308.2149, 2013 (revised 2014).
  10. MathScheme: Project description Abstract PDF Springer Link
    J. Carette, W. M. Farmer, and R. O'Connor
    In: J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds., Intelligent Computer Mathematics (CICM 2011), Lecture Notes in Computer Science (LNCS), 6824:287–288, 2011.
  11. The MathScheme library: Some preliminary experiments Abstract PDF
    J. Carette, W. M. Farmer, F. Jeremic, V. Maccio, R. O'Connor, and Q. M. Tran
    In: A. Asperti, J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds., Conference on Intelligent Computer Mathematics Work-in-Progress Papers Proceedings, Technical Report UBLCS-2011-04, pp. 10–22, University of Bologna, 2011.
    Preprint: arXiv:1106.1862, 2011.
  12. High-level theories Abstract PDF Springer Link
    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.
  13. Biform theories in Chiron Abstract PDF Springer Link
    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.
  14. A rational reconstruction of a system for experimental mathematics Abstract PDF Springer Link
    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.
  15. 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.
  16. Trustable communication between mathematics systems Abstract PDF
    J. Carette, W. M. Farmer, and J. Wajs
    SQRL Report No. 41, 22 pp., McMaster University, 2004.
    This is an extended, revised version of the paper below with the same name.
  17. Trustable communication between mathematics systems Abstract 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.
  18. An overview of a Formal Framework for Managing Mathematics Abstract PDF Springer Link
    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.
  19. 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.
  20. A proposal for the development of an interactive mathematics laboratory for mathematics education 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.
  21. Transformers for symbolic computation and formal deduction Abstract 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.
  22. 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.

C. Tetrapod Project

  1. The space of mathematical software systems — A survey of paradigmatic systems Abstract
    K. Berčič, J. Carette, W. M. Farmer, M. Kohlhase, D. Müller, F. Rabe, and Y. Sharoda
    arXiv:2002.04955, 2020.
  2. Big math and the one-brain barrier: A position paper and architecture proposal Abstract PDF Springer Link
    J. Carette, W. M. Farmer, M. Kohlhase, and F. Rabe
    The Mathematical Intelligencer, 43:78--87, 2021.
  3. Realms: A structure for consolidating knowledge about mathematical theories Abstract PDF Springer Link
    J. Carette, W. M. Farmer, and M. Kohlhase
    In: S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban, eds., Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science (LNCS), 8543:252–266, 2014.
    Preprint: arXiv:1405.5956, 2014.

D. IMPS Interactive Mathematical Proof System

  1. Panoptes: An exploration tool for formal proofs Abstract PDF ScienceDirect
    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.
  2. IMPS Abstract Springer Link
    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 PDF ScienceOpen
    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 PDF Springer Link
    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 ScienceDirect
    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 PDF Springer Link
    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. Theory interpretation in simple type theory Abstract PDF Springer Link
    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.
  8. Reasoning with contexts Springer Link
    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.
  9. The IMPS User's Manual HTML PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Technical Report M-93B138, 289 pp., The MITRE Corporation, November 1993.
  10. IMPS: An Interactive Mathematical Proof System Abstract PDF Springer Link
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Automated Reasoning, 11:213–248, 1993.
  11. A simple type theory with partial functions and subtypes Abstract ScienceDirect
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211–240, 1993.
  12. 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.
  13. Little theories Abstract PDF Springer Link
    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.
  14. Theory interpretations in computerized mathematics
    W. M. Farmer
    Journal of Symbolic Logic, 57:356, 1992.
    Abstract.
  15. IMPS: System description PDF Springer Link
    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.
  16. Two computer-supported proofs in metric space topology PDF
    W. M. Farmer and F. J. Thayer
    Notices of the American Mathematical Society, 38:1133–1138, 1991.
  17. A partial functions version of Church's simple theory of types Abstract Cambridge Core
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269–1291, 1990.
  18. IMPS: An Interactive Mathematical Proof System (system description) Springer Link
    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.
    Extended Abstract.

E. Simple Type Theory

  1. Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas Springer Link
    W. M. Farmer
    Computer Science Foundations and Applied Logic, Birkhäuser/Springer, 2023.
  2. Incorporating quotation and evaluation into Church's type theory Abstract PDF ScienceDirect
    W. M. Farmer
    Information and Computation, 260:9–50, 2018.
    Preprint: arXiv:1612.02785 (74 pp.), 2016 (revised 2018).
  3. Theory morphisms in Church's type theory with quotation and evaluation Abstract PDF Springer Link
    W. M. Farmer
    In: H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science (LNCS), 10383:147–162, 2017.
    Preprint: arXiv:1703.02117, 2017.
  4. Incorporating quotation and evaluation into Church's type theory: Syntax and semantics Abstract PDF Springer Link
    W. M. Farmer
    In: M. Kohlhase et al., eds., Intelligent Computer Mathematics (CICM 2016), Lecture Notes in Computer Science (LNCS), 9791:83–98, 2016. This is a preliminary version of the Information and Computation paper.
    Preprint: arXiv:1605.07068, 2016.
  5. Simple type theory with undefinedness, quotation, and evaluation Abstract PDF
    W. M. Farmer
    McSCert Report 13, 87 pp., McMaster University, 2014 (revised 2016).
    Preprint: arXiv:1406.6706, 2014 (revised 2016).
  6. Andrews' type system with undefinedness Abstract PDF
    W. M. Farmer
    In: C. Benzmüller, 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.
    Preprint: arXiv:1406.7492, 2014.
  7. The seven virtues of simple type theory Abstract PDF ScienceDirect
    W. M. Farmer
    Journal of Applied Logic, 6:267–286, 2008.
  8. Formalizing undefinedness arising in calculus Abstract PDF Springer Link
    W. M. Farmer
    In: D. Basin and M. Rusinowitch, eds., Automated Reasoning, Lecture Notes in Computer Science (LNCS), 3097:475–489, 2004.
  9. A basic extended simple type theory Abstract PDF
    W. M. Farmer
    SQRL Report No. 14, 12 pp., McMaster University, 2003 (revised 2004).
  10. A simple type theory with partial functions and subtypes Abstract ScienceDirect
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211–240, 1993.
  11. 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.
  12. A partial functions version of Church's simple theory of types Abstract Cambridge Core
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269–1291, 1990.

F. Set Theories for Mechanized Mathematics

  1. Chiron: A set theory with types, undefinedness, quotation, and evaluation Abstract PDF
    W. M. Farmer
    SQRL Report No. 38, 154 pp., McMaster University, 2007 (revised 2012).
    Preprint: arXiv:1305.6206, 2013.
  2. Chiron: A multi-paradigm logic Abstract 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.
  3. STMM: A Set Theory for Mechanized Mathematics Abstract PDF Springer Link
    W. M. Farmer
    Journal of Automated Reasoning, 26:269–289, 2001.
  4. A set theory with support for partial functions Abstract PDF Springer Link
    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.
  5. 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.
  6. 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.

G. Undefinedness and Partial Functions

  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 PDF
    W. M. Farmer
    In: C. Benzmüller, 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.
    Preprint: arXiv:1406.7492, 2014.
  3. Formalizing undefinedness arising in calculus Abstract PDF Springer Link
    W. M. Farmer
    In: D. Basin and M. Rusinowitch, eds., Automated Reasoning, Lecture Notes in Computer Science (LNCS), 3097:475–489, 2004.
  4. A set theory with support for partial functions Abstract PDF Springer Link
    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.
  5. A scheme for defining partial higher-order functions by recursion Abstract PDF ScienceOpen
    W. M. Farmer
    In: A. Butterfield, ed., 3rd Irish Workshop on Formal Methods, 13 pp., electronic Workshops in Computing, Springer-Verlag, 1999.
  6. Mechanizing the traditional approach to partial functions Abstract 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.
  7. Reasoning about partial functions with the aid of a computer Abstract PDF Springer Link
    W. M. Farmer
    Erkenntnis, 43:279–294, 1995.
  8. A simple type theory with partial functions and subtypes Abstract ScienceDirect
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211–240, 1993.
  9. 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.
  10. A partial functions version of Church's simple theory of types Abstract Cambridge Core
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269–1291, 1990.

H. Logics with Quotation and Evaluation

  1. Towards specifying symbolic computation Abstract PDF Springer Link
    J. Carette and W. M. Farmer
    In: C. Kalisyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen, eds., Intelligent Computer Mathematics (CICM 2019), Lecture Notes in Computer Science (LNCS), 11617:109–124, 2019.
    Preprint: arXiv:1904.02729, 2019.
  2. Incorporating quotation and evaluation into Church's type theory Abstract PDF ScienceDirect
    W. M. Farmer
    Information and Computation, 260:9–50, 2018.
    Preprint: arXiv:1612.02785 (74 pp.), 2016 (revised 2018).
  3. HOL Light QE Abstract PDF Springer Link
    J. Carette, W. M. Farmer, and P. Laskowski
    In: J. Avigad and A. Mahboubi, eds., Interactive Theorem Proving (ITP 2018), Lecture Notes in Computer Science (LNCS), 10895:215–234, 2018.
    Preprint: arXiv:1802.00405, 2018.
  4. Formalizing mathematical knowledge as a biform theory graph: A case study Abstract PDF Springer Link
    J. Carette and W. M. Farmer
    In: H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science (LNCS), 10383:9–24, 2017 (without appendices).
    Preprint with appendices: arXiv:1704.02253 (43 pp.), 2017.
  5. Theory morphisms in Church's type theory with quotation and evaluation Abstract PDF Springer Link
    W. M. Farmer
    In: H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science (LNCS), 10383:147–162, 2017.
    Preprint: arXiv:1703.02117, 2017.
  6. Incorporating quotation and evaluation into Church's type theory: Syntax and semantics Abstract PDF Springer Link
    W. M. Farmer
    In: M. Kohlhase et al., eds., Intelligent Computer Mathematics (CICM 2016), Lecture Notes in Computer Science (LNCS), 9791:83–98, 2016. This is a preliminary version of the Information and Computation paper.
    Preprint: arXiv:1605.07068, 2016.
  7. Simple type theory with undefinedness, quotation, and evaluation Abstract PDF
    W. M. Farmer
    McSCert Report 13, 87 pp., McMaster University, 2014 (revised 2016).
    Preprint: arXiv:1406.6706, 2014 (revised 2016).
  8. The formalization of syntax-based mathematical algorithms using quotation and evaluation Abstract PDF Springer Link
    W. M. Farmer
    In: J. Carette et al., eds., Intelligent Computer Mathematics (CICM 2013), Lecture Notes in Computer Science (LNCS), 7961:35–50, 2013.
    Preprint: arXiv:1305.6052, 2013.
  9. Frameworks for reasoning about syntax that utilize quotation and evaluation Abstract PDF
    W. M. Farmer and P. Larjani
    McSCert Report 9, 38 pp., McMaster University, 2013 (revised 2014).
    Preprint: arXiv:1308.2149, 2013 (revised 2014).
  10. Chiron: A set theory with types, undefinedness, quotation, and evaluation Abstract PDF
    W. M. Farmer
    SQRL Report No. 38, 154 pp., McMaster University, 2007 (revised 2012).
    Preprint: arXiv:1305.6206, 2013.
  11. Chiron: A multi-paradigm logic Abstract 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.

I. Little Theories Method

  1. Formalizing mathematical knowledge as a biform theory graph: A case study Abstract PDF Springer Link
    J. Carette and W. M. Farmer
    In: H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science (LNCS), 10383:9–24, 2017 (without appendices).
    Preprint with appendices: arXiv:1704.02253 (43 pp.), 2017.
  2. Theory morphisms in Church's type theory with quotation and evaluation Abstract PDF Springer Link
    W. M. Farmer
    In: H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer Mathematics (CICM 2017), Lecture Notes in Computer Science (LNCS), 10383:147–162, 2017.
    Preprint: arXiv:1703.02117, 2017.
  3. Realms: A structure for consolidating knowledge about mathematical theories Abstract PDF Springer Link
    J. Carette, W. M. Farmer, and M. Kohlhase
    In: S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban, eds., Intelligent Computer Mathematics (CICM 2014), Lecture Notes in Computer Science (LNCS), 8543:252–266, 2014.
    Preprint: arXiv:1405.5956, 2014.
  4. Modules for a large library of formalized mathematics
    W. M. Farmer
    AMS Special Session on Formal Mathematics for Mathematicians: Developing Large Repositories of Advanced Mathematics, JMM 2011, JMM abstract 1067-03-1782, 2011.
    Abstract.
  5. An infrastructure for intertheory reasoning Abstract PDF Springer Link
    W. M. Farmer
    In: D. McAllester, ed., Automated Deduction—CADE-17, Lecture Notes in Computer Science (LNCS), 1831:115–131, 2000.
  6. Perspective switching using theories and interpretations 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.
    Extended Abstract.
  7. Theory interpretation in simple type theory Abstract PDF Springer Link
    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.
  8. A general method for safely overwriting theories in mechanized mathematics systems Abstract PDF
    W. M. Farmer
    Technical Report, 21 pp., The MITRE Corporation, 1994.
  9. 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.
    Extended Abstract.
  10. Little theories Abstract PDF Springer Link
    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.
  11. Theory interpretations in computerized mathematics
    W. M. Farmer
    Journal of Symbolic Logic, 57:356, 1992.
    Abstract.
  12. Abstract data types in many-sorted second-order logic
    W. M. Farmer
    Technical Report M87-64, 29 pp., The MITRE Corporation, October 1987.

J. Mathematical Knowledge Management (MKM)

  1. A new style of proof for mathematics organized as a network of axiomatic theories Abstract PDF
    W. M. Farmer
    arXiv:1806.00810, 2018.
    This is an extended version of the paper below.
  2. A new style of mathematical proof Abstract PDF Springer Link
    W. M. Farmer
    In: J. H. Davenport, M. Kauers, G. Labahn, and J. Urban, eds., Mathematical Software—ICMS 2018, Lecture Notes in Computer Science (LNCS), 10931:175–181, 2018.
    Preprint: arXiv:1806.00810, 2018.
  3. We need a better style of proof Abstract
    W. M. Farmer
    In: G. Dowek, C. Dubois, B. Pientka, and F. Rabe, eds, Universality of Proofs (Dagstuhl Seminar 16421), Dagstuhl Reports, 6:82, 2017.
    Abstract.
  4. A review of mathematical knowledge management Abstract PDF Springer Link
    J. Carette and W. M. Farmer
    In: J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt, eds., Intelligent Computer Mathematics (CICM 2009), Lecture Notes in Computer Science (LNCS), 5625:233–246, 2009.
  5. 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
  6. MKM: A new interdisciplinary field of research Abstract PDF ACM Digital Library
    W. M. Farmer
    ACM SIGSAM Bulletin, 38:47–52, 2004.

K. Formal Methods

  1. FCL: A formal language for writing contracts Abstract PDF Springer Link
    W. M. Farmer and Q. Hu
    In: S. H. Rubin and T. Bouabana Tebibel, eds., Quality Software Through Reuse and Integration, pp. 190–208, Springer, 2018. This is a extended version of the paper below.
  2. A formal language for writing contracts Abstract PDF IEEE Xplore
    W. M. Farmer and Q. Hu
    In: 2016 IEEE International Conference on Information Reuse and Integration, 8 pp., IEEE, 2016.
  3. A verified compiler for Multithreaded PreScheme Abstract
    W. M. Farmer and J. D. Ramsdell
    Technical Report, 180 pp., The MITRE Corporation, 1996.
  4. Formal numerical program analysis Abstract PDF
    W. M. Farmer and F. J. Thayer
    Technical Report, 52 pp., The MITRE Corporation, 1994.
  5. 8 papers on the VLISP verified programming language implementation
    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.
  6. Towards a discipline for developing verified software Abstract PDF
    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.

L. Security of Mobile Agents

  1. Security for mobile agents: Issues and requirements Abstract 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 PDF Springer Link
    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.

M. Graph Rewriting and Combinatory Algebra

  1. Redex capturing in term graph rewriting (concise version) Springer Link
    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 PDF World Scientific
    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 ACM Digital Library
    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.

N. Higher-Order Unification

  1. Simple second-order languages for which unification is undecidable Abstract ScienceDirect
    W. M. Farmer
    Theoretical Computer Science, 87:25–41, 1991.
  2. A unification algorithm for second-order monadic terms Abstract ScienceDirect
    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.

O. Length of Proofs

  1. The Kreisel length-of-proof problem Abstract Springer Link
    W. M. Farmer
    In: J. Franco, J. M. Dunn, and W. H. Wheeler, eds., Logic and Combinatorics, 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 ScienceDirect
    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.

P. 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 IEEE Computer Society Digital Library
    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. A proposal for the development of an interactive mathematics laboratory for mathematics education 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.
  4. 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.

Q. Miscellaneous

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

R. Edited Conference Proceedings

  1. Workshop Papers at 12th Conference on Intelligent Computer Mathematics (CICM 2019) CEUR Workshop Proceedings
    E. Brady, J. Davenport, W. M. Farmer, C. Kaliszyk, A. Kohlhase, M. Kohlhase, D. Müller, K. Pak, eds.
    CEUR Workshop Proceedings, Vol. 2634, 2020.
  2. Workshop Papers at 11th Conference on Intelligent Computer Mathematics (CICM 2018) CEUR Workshop Proceedings
    O. Hasan, A. Youssef, A. Naumowicz, W. M. Farmer, C. Kaliszyk, D. Gallois-Wong, F. Rabe, G. Dos Reis, G. O. Passmore, J. H. Davenport, M. Pfeiffer, M. Kohlhase, S. Autexier, S. Tahar, T. Koprucki, U. Siddique, W. Neuper, W. Windsteiger, W. Schreiner, W. Sperber, and Z. Kovàcs, eds.
    CEUR Workshop Proceedings, Vol. 2307, 2019.
  3. Intelligent Computer Mathematics (11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings) Springer Link
    F. Rabe, W. Farmer, O. Hasan, G. Passmore, and A. Youssef, eds.
    Lecture Notes in Computer Science (LNCS), 11006:1–287, 2018.
  4. Intelligent Computer Mathematics (18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings) Springer Link
    J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds.
    Lecture Notes in Computer Science (LNCS), 6824:1–312, 2011.
  5. Conference on Intelligent Computer Mathematics Work-in-Progress Papers Proceedings
    A. Asperti, J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds.
    Technical Report UBLCS-2011-04, University of Bologna, 2011.
  6. Mathematical Knowledge Management (5th International Conference, MKM 2006, Wokingham, UK, August 2006, Proceedings) Springer Link
    J. M. Borwein and W. M. Farmer, eds.
    Lecture Notes in Computer Science (LNCS), 4108:1–295, 2006.
  7. Proceeding of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005) ACM Digital Library
    J. Carette and W. M. Farmer, eds.
    Electronic Notes in Theoretical Computer Science (ENTCS), 151:1–178, 2006.
  8. 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.

S. Reviews

  1. Review of Jan Krajícek, On the number of steps in proofs, Annals of Pure and Applied Logic, 41:153–178, 1989. PhilPapers
    W. M. Farmer, Journal of Symbolic Logic, 56:334–335, 1991.
  2. Review of Jan Krajícek and Pavel Pudlák, The number of proof lines and the size of proofs in first order logic, Archive for Mathematical Logic, 27:69–84, 1988. Cambridge Core
    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. Cambridge Core
    W. M. Farmer, Journal of Symbolic Logic, 53:1258–1259, 1988.