A unification algorithm for second-order monadic terms. - William M. Farmer (Ann. Pure Appl. Log., 1988)

Minutes of the 4th annual LICS business meeting. - William M. Farmer; A. J. Kfoury (SIGACT News, 1989)

Redex Capturing in Term Graph Rewriting. - William M. Farmer; Ronald J. Watro (Int. J. Found. Comput. Sci., 1990)

A Partial Functions Version of Church's Simple Theory of Types. - William M. Farmer (J. Symb. Log., 1990)

A Correctness Proof for Combinator Reduction with Cycles. - William M. Farmer; John D. Ramsdell; Ronald J. Watro (ACM Trans. Program. Lang. Syst., 1990)

Redex Capturing in Term Graph Rewriting (Concise Version). - William M. Farmer; Ronald J. Watro (RTA, 1991)

A Unification-Theoretic Method for Investigating the k-Provability Problem. - William M. Farmer (Ann. Pure Appl. Log., 1991)

Simple Second-order Languages for which Unification is Undecidable. - William M. Farmer (Theor. Comput. Sci., 1991)

Little Theories. - William M. Farmer; Joshua D. Guttman; F. Javier Thayer (CADE, 1992)

IMPS: System Description. - William M. Farmer; Joshua D. Guttman; F. Javier Thayer (CADE, 1992)

The Kreisel Length-of-Proof Problem. - William M. Farmer (Ann. Math. Artif. Intell., 1992)

Reasoning with Contexts. - William M. Farmer; Joshua D. Guttman; F. Javier Thayer (DISCO, 1993)

Theory Interpretation in Simple Type Theory. - William M. Farmer (HOA, 1993)

A Simple Type Theory with Partial Functions and Subtypes. - William M. Farmer (Ann. Pure Appl. Log., 1993)

IMPS: An Interactive Mathematical Proof System. - William M. Farmer; Joshua D. Guttman; F. Javier Thayer (J. Autom. Reason., 1993)

Proof Script Pragmatics in IMPS. - William M. Farmer; Joshua D. Guttman; Mark E. Nadel; F. Javier Thayer (CADE, 1994)

Context in Mathematical Reasoning and Computation. - William M. Farmer; Joshua D. Guttman; F. Javier Thayer (J. Symb. Comput., 1995)

IMPS: An Updated System Description. - William M. Farmer; Joshua D. Guttman; F. Javier Thayer (CADE, 1996)

Security for Mobile Agents: Authentication and State Appraisal. - William M. Farmer; Joshua D. Guttman; Vipin Swarup (ESORICS, 1996)

For a Massive Number of Massively Parallel Machines: What are the Target Applications, Who are the Target Users, and What New R&D is Needed to Hit the Target? - William M. Farmer; Richard F. Freund; Mark Furtney; Paul Messina; Lionel M. Ni; Charles L. Seitz; Marc Snir (IPPS, 1996)

A Scheme for Defining Partial Higher-Order Functions by Recursion. - William M. Farmer (IWFM, 1999)

An Infrastructure for Intertheory Reasoning. - William M. Farmer (CADE, 2000)

A Set Theory with Support for Partial Functions. - William M. Farmer; Joshua D. Guttman (Stud Logica, 2000)

STMM: A Set Theory for Mechanized Mathematics. - William M. Farmer (J. Autom. Reason., 2001)

An Overview of a Formal Framework for Managing Mathematics. - William M. Farmer; Martin von Mohrenschildt (Ann. Math. Artif. Intell., 2003)

Formalizing Undefinedness Arising in Calculus. - William M. Farmer (IJCAR, 2004)

MKM: a new interdisciplinary field of research. - William M. Farmer (SIGSAM Bull., 2004)

Preface. - Jacques Carette; William M. Farmer (Calculemus, 2005)

IMPS. - William M. Farmer (The Seventeen Provers of the World, 2006)

A Rational Reconstruction of a System for Experimental Mathematics. - Jacques Carette; William M. Farmer; Volker Sorge (Calculemus/MKM, 2007)

Biform Theories in Chiron. - William M. Farmer (Calculemus/MKM, 2007)

High-Level Theories. - Jacques Carette; William M. Farmer (AISC/MKM/Calculemus, 2008)

Panoptes: An Exploration Tool for Formal Proofs. - William M. Farmer; Orlin G. Grigorov (UITP@TPHOLs, 2008)

The seven virtues of simple type theory. - William M. Farmer (J. Appl. Log., 2008)

A Review of Mathematical Knowledge Management. - Jacques Carette; William M. Farmer (Calculemus/MKM, 2009)

MathScheme: Project Description. - Jacques Carette; William M. Farmer; Russell O'Connor (Calculemus/MKM, 2011)

The MathScheme Library: Some Preliminary Experiments - Jacques Carette; William M. Farmer; Filip Jeremic; Vincent Maccio; Russell O'Connor; Quang M. Tran (CoRR, 2011)

Mathematical Knowledge Management. - William M. Farmer (Encyclopedia of Knowledge Management, 2011)

The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. - William M. Farmer (MKM/Calculemus/DML, 2013)

Frameworks for Reasoning about Syntax that Utilize Quotation and Evaluation. - William M. Farmer; Pouya Larjani (CoRR, 2013)

Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation - William M. Farmer (CoRR, 2013)

Realms: A Structure for Consolidating Knowledge about Mathematical Theories. - Jacques Carette; William M. Farmer; Michael Kohlhase (CICM, 2014)

Meaning Formulas for Syntax-Based Mathematical Algorithms. - William M. Farmer (SCSS, 2014)

Simple Type Theory with Undefinedness, Quotation, and Evaluation. - William M. Farmer (CoRR, 2014)

Andrews' Type Theory with Undefinedness. - William M. Farmer (CoRR, 2014)

A Formal Language for Writing Contracts. - William M. Farmer; Qian Hu (IRI, 2016)

Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics. - William M. Farmer (CICM, 2016)

Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. - Jacques Carette; William M. Farmer (CICM, 2017)

Theory Morphisms in Church's Type Theory with Quotation and Evaluation. - William M. Farmer (CICM, 2017)

A New Style of Mathematical Proof. - William M. Farmer (ICMS, 2018)

HOL Light QE. - Jacques Carette; William M. Farmer; Patrick Laskowski (ITP, 2018)

Biform Theories: Project Description. - Jacques Carette; William M. Farmer; Yasmine Sharoda (CICM, 2018)

Incorporating quotation and evaluation into Church's type theory. - William M. Farmer (Inf. Comput., 2018)

Towards Specifying Symbolic Computation. - Jacques Carette; William M. Farmer (CICM, 2019)

Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal. - Jacques Carette; William M. Farmer; Michael Kohlhase; Florian Rabe 001 (CoRR, 2019)

Leveraging the Information Contained in Theory Presentations. - Jacques Carette; William M. Farmer; Yasmine Sharoda (CICM, 2020)

The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. - Katja Bercic; Jacques Carette; William M. Farmer; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001; Yasmine Sharoda (CoRR, 2020)

Formal Mathematics for the Masses (short paper). - William M. Farmer (CICM Workshops, 2021)

Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas - William M. Farmer (Springer, 2023)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory. - William M. Farmer; Dennis Y. Zvigelsky (CoRR, 2023)

Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas, Second Editiontion - William M. Farmer (Springer, 2025)