William M. Farmer

According to our database, William M. Farmer authored at least 59 papers between 1988 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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

William M. Farmer

Springer, ISBN: 978-3-031-21111-9, 2023

2020

The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems.

Katja Bercic, Jacques Carette, William M. Farmer, Michael Kohlhase, Dennis Müller, Florian Rabe, Yasmine Sharoda

CoRR, 2020

Leveraging the Information Contained in Theory Presentations.

Jacques Carette, William M. Farmer, Yasmine Sharoda

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019

Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal.

Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe

CoRR, 2019

Towards Specifying Symbolic Computation.

Jacques Carette, William M. Farmer

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

2018

Incorporating quotation and evaluation into Church's type theory.

William M. Farmer

Inf. Comput., 2018

Biform Theories: Project Description.

Jacques Carette, William M. Farmer, Yasmine Sharoda

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

HOL Light QE.

Jacques Carette, William M. Farmer, Patrick Laskowski

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

A New Style of Mathematical Proof.

William M. Farmer

Proceedings of the Mathematical Software - ICMS 2018, 2018

2017

Theory Morphisms in Church's Type Theory with Quotation and Evaluation.

William M. Farmer

Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study.

Jacques Carette, William M. Farmer

Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

2016

Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics.

William M. Farmer

Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

A Formal Language for Writing Contracts.

William M. Farmer, Qian Hu

Proceedings of the 17th IEEE International Conference on Information Reuse and Integration, 2016

2014

Andrews' Type Theory with Undefinedness.

William M. Farmer

CoRR, 2014

Simple Type Theory with Undefinedness, Quotation, and Evaluation.

William M. Farmer

CoRR, 2014

Meaning Formulas for Syntax-Based Mathematical Algorithms.

William M. Farmer

Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

Realms: A Structure for Consolidating Knowledge about Mathematical Theories.

Jacques Carette, William M. Farmer, Michael Kohlhase

Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

2013

Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation

William M. Farmer

CoRR, 2013

Frameworks for Reasoning about Syntax that Utilize Quotation and Evaluation.

William M. Farmer, Pouya Larjani

CoRR, 2013

The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation.

William M. Farmer

Proceedings of the Intelligent Computer Mathematics, 2013

2011

Mathematical Knowledge Management.

William M. Farmer

Proceedings of the Encyclopedia of Knowledge Management, Second Edition, 2011

The MathScheme Library: Some Preliminary Experiments

Jacques Carette, William M. Farmer, Filip Jeremic, Vincent Maccio, Russell O'Connor, Quang M. Tran

CoRR, 2011

MathScheme: Project Description.

Jacques Carette, William M. Farmer, Russell O'Connor

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2009

A Review of Mathematical Knowledge Management.

Jacques Carette, William M. Farmer

Proceedings of the Intelligent Computer Mathematics, 2009

2008

The seven virtues of simple type theory.

William M. Farmer

J. Appl. Log., 2008

Panoptes: An Exploration Tool for Formal Proofs.

William M. Farmer, Orlin G. Grigorov

Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

High-Level Theories.

Jacques Carette, William M. Farmer

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

Biform Theories in Chiron.

William M. Farmer

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

A Rational Reconstruction of a System for Experimental Mathematics.

Jacques Carette, William M. Farmer, Volker Sorge

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

IMPS.

William M. Farmer

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

Preface.

Jacques Carette, William M. Farmer

Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, 2005

2004

MKM: a new interdisciplinary field of research.

William M. Farmer

SIGSAM Bull., 2004

Formalizing Undefinedness Arising in Calculus.

William M. Farmer

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

An Overview of a Formal Framework for Managing Mathematics.

William M. Farmer, Martin von Mohrenschildt

Ann. Math. Artif. Intell., 2003

2001

STMM: A Set Theory for Mechanized Mathematics.

William M. Farmer

J. Autom. Reason., 2001

2000

A Set Theory with Support for Partial Functions.

William M. Farmer, Joshua D. Guttman

Stud Logica, 2000

An Infrastructure for Intertheory Reasoning.

William M. Farmer

Proceedings of the Automated Deduction, 2000

1999

A Scheme for Defining Partial Higher-Order Functions by Recursion.

William M. Farmer

Proceedings of the 3rd Irish Workshop on Formal Methods, Galway, Ireland, July 1999, 1999

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

Proceedings of IPPS '96, 1996

Security for Mobile Agents: Authentication and State Appraisal.

William M. Farmer, Joshua D. Guttman, Vipin Swarup

Proceedings of the Computer Security, 1996

IMPS: An Updated System Description.

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Context in Mathematical Reasoning and Computation.

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

J. Symb. Comput., 1995

1994

Proof Script Pragmatics in IMPS.

William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

IMPS: An Interactive Mathematical Proof System.

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

J. Autom. Reason., 1993

A Simple Type Theory with Partial Functions and Subtypes.

William M. Farmer

Ann. Pure Appl. Log., 1993

Theory Interpretation in Simple Type Theory.

William M. Farmer

Proceedings of the Higher-Order Algebra, 1993

Reasoning with Contexts.

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1993

1992

The Kreisel Length-of-Proof Problem.

William M. Farmer

Ann. Math. Artif. Intell., 1992

IMPS: System Description.

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

Proceedings of the Automated Deduction, 1992

Little Theories.

William M. Farmer, Joshua D. Guttman, F. Javier Thayer

Proceedings of the Automated Deduction, 1992

1991

Simple Second-order Languages for which Unification is Undecidable.

William M. Farmer

Theor. Comput. Sci., 1991

A Unification-Theoretic Method for Investigating the k-Provability Problem.

William M. Farmer

Ann. Pure Appl. Log., 1991

Redex Capturing in Term Graph Rewriting (Concise Version).

William M. Farmer, Ronald J. Watro

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

1990

A Correctness Proof for Combinator Reduction with Cycles.

William M. Farmer, John D. Ramsdell, Ronald J. Watro

ACM Trans. Program. Lang. Syst., 1990

A Partial Functions Version of Church's Simple Theory of Types.

William M. Farmer

J. Symb. Log., 1990

Redex Capturing in Term Graph Rewriting.

William M. Farmer, Ronald J. Watro

Int. J. Found. Comput. Sci., 1990

1989

Minutes of the 4th annual LICS business meeting.

William M. Farmer, A. J. Kfoury

SIGACT News, 1989

1988

A unification algorithm for second-order monadic terms.

William M. Farmer

Ann. Pure Appl. Log., 1988