default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDWilliam M. Farmer
Person information
- affiliation: McMaster University, Hamilton, Ontario, Canada
Other persons with a similar name
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[b1]William M. Farmer:
Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas. Springer 2023, ISBN 978-3-031-21111-9, pp. 1-215- [i19]William M. Farmer, Dennis Y. Zvigelsky:
Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory. CoRR abs/2312.05658 (2023) - 2021
- [c33]William M. Farmer:
Formal Mathematics for the Masses (short paper). CICM Workshops 2021 - 2020
- [c32]Jacques Carette, William M. Farmer, Yasmine Sharoda:
Leveraging the Information Contained in Theory Presentations. CICM 2020: 55-70 - [e6]Edwin C. Brady, James H. Davenport, William M. Farmer, Cezary Kaliszyk, Andrea Kohlhase, Michael Kohlhase, Dennis Müller, Karol Pak, Claudio Sacerdoti Coen:
Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague, Czech Republic, July 8-12, 2019. CEUR Workshop Proceedings 2634, CEUR-WS.org 2020 [contents] - [i18]Katja Bercic, Jacques Carette, William M. Farmer, Michael Kohlhase, Dennis Müller
, Florian Rabe, Yasmine Sharoda:
The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. CoRR abs/2002.04955 (2020) - [i17]Jacques Carette, William M. Farmer, Yasmine Sharoda:
Leveraging the Information Contained in Theory Presentations. CoRR abs/2006.09292 (2020)
2010 – 2019
- 2019
- [c31]Jacques Carette, William M. Farmer:
Towards Specifying Symbolic Computation. CICM 2019: 109-124 - [e5]Osman Hasan, Abdou Youssef, Adam Naumowicz, William M. Farmer, Cezary Kaliszyk, Diane Gallois-Wong, Florian Rabe, Gabriel Dos Reis, Grant O. Passmore, James H. Davenport, Markus Pfeiffer, Michael Kohlhase, Serge Autexier, Sofiène Tahar, Thomas Koprucki, Umair Siddique, Walther Neuper, Wolfgang Windsteiger, Wolfgang Schreiner, Wolfram Sperber, Zoltán Kovács:
Joint Proceedings of the CME-EI, FMM, CAAT, FVPS, M3SRD, OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2018 co-located with the 11th Conference on Intelligent Computer Mathematics (CICM 2018), Hagenberg, Austria, August 13-17, 2018. CEUR Workshop Proceedings 2307, CEUR-WS.org 2019 [contents] - [i16]Jacques Carette, William M. Farmer:
Towards Specifying Symbolic Computation. CoRR abs/1904.02729 (2019) - [i15]Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe:
Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal. CoRR abs/1904.10405 (2019) - 2018
- [j17]William M. Farmer:
Incorporating quotation and evaluation into Church's type theory. Inf. Comput. 260: 9-50 (2018) - [c30]William M. Farmer:
A New Style of Mathematical Proof. ICMS 2018: 175-181 - [c29]Jacques Carette, William M. Farmer, Patrick Laskowski:
HOL Light QE. ITP 2018: 215-234 - [c28]Jacques Carette, William M. Farmer, Yasmine Sharoda:
Biform Theories: Project Description. CICM 2018: 76-86 - [e4]Florian Rabe, William M. Farmer, Grant O. Passmore, Abdou Youssef:
Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings. Lecture Notes in Computer Science 11006, Springer 2018, ISBN 978-3-319-96811-7 [contents] - [i14]Jacques Carette, William M. Farmer, Patrick Laskowski:
HOL Light QE. CoRR abs/1802.00405 (2018) - [i13]Jacques Carette, William M. Farmer, Yasmine Sharoda:
Biform Theories: Project Description. CoRR abs/1805.02709 (2018) - [i12]William M. Farmer:
A New Style of Mathematical Proof. CoRR abs/1806.00810 (2018) - 2017
- [c27]Jacques Carette, William M. Farmer:
Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. CICM 2017: 9-24 - [c26]William M. Farmer:
Theory Morphisms in Church's Type Theory with Quotation and Evaluation. CICM 2017: 147-162 - [i11]William M. Farmer:
Theory Morphisms in Church's Type Theory with Quotation and Evaluation. CoRR abs/1703.02117 (2017) - [i10]Jacques Carette, William M. Farmer:
Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. CoRR abs/1704.02253 (2017) - 2016
- [c25]William M. Farmer, Qian Hu:
A Formal Language for Writing Contracts. IRI 2016: 134-141 - [c24]William M. Farmer:
Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics. CICM 2016: 83-98 - [i9]William M. Farmer:
Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics. CoRR abs/1605.07068 (2016) - [i8]William M. Farmer:
Incorporating Quotation and Evaluation Into Church's Type Theory. CoRR abs/1612.02785 (2016) - 2014
- [c23]Jacques Carette, William M. Farmer, Michael Kohlhase:
Realms: A Structure for Consolidating Knowledge about Mathematical Theories. CICM 2014: 252-266 - [c22]William M. Farmer:
Meaning Formulas for Syntax-Based Mathematical Algorithms. SCSS 2014: 10-11 - [i7]Jacques Carette, William M. Farmer, Michael Kohlhase:
Realms: A Structure for Consolidating Knowledge about Mathematical Theories. CoRR abs/1405.5956 (2014) - [i6]William M. Farmer:
Simple Type Theory with Undefinedness, Quotation, and Evaluation. CoRR abs/1406.6706 (2014) - [i5]William M. Farmer:
Andrews' Type Theory with Undefinedness. CoRR abs/1406.7492 (2014) - 2013
- [c21]William M. Farmer:
The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. MKM/Calculemus/DML 2013: 35-50 - [i4]William M. Farmer:
The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. CoRR abs/1305.6052 (2013) - [i3]William M. Farmer:
Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation. CoRR abs/1305.6206 (2013) - [i2]William M. Farmer, Pouya Larjani:
Frameworks for Reasoning about Syntax that Utilize Quotation and Evaluation. CoRR abs/1308.2149 (2013) - 2011
- [c20]Jacques Carette, William M. Farmer, Russell O'Connor:
MathScheme: Project Description. Calculemus/MKM 2011: 287-288 - [e3]James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe:
Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings. Lecture Notes in Computer Science 6824, Springer 2011, ISBN 978-3-642-22672-4 [contents] - [r1]William M. Farmer:
Mathematical Knowledge Management. Encyclopedia of Knowledge Management 2011: 1082-1089 - [i1]Jacques Carette, William M. Farmer, Filip Jeremic, Vincent Maccio, Russell O'Connor, Quang M. Tran:
The MathScheme Library: Some Preliminary Experiments. CoRR abs/1106.1862 (2011)
2000 – 2009
- 2009
- [c19]Jacques Carette, William M. Farmer:
A Review of Mathematical Knowledge Management. Calculemus/MKM 2009: 233-246 - 2008
- [j16]William M. Farmer:
The seven virtues of simple type theory. J. Appl. Log. 6(3): 267-286 (2008) - [c18]Jacques Carette, William M. Farmer:
High-Level Theories. AISC/MKM/Calculemus 2008: 232-245 - [c17]William M. Farmer, Orlin G. Grigorov:
Panoptes: An Exploration Tool for Formal Proofs. UITP@TPHOLs 2008: 39-48 - 2007
- [c16]Jacques Carette, William M. Farmer, Volker Sorge:
A Rational Reconstruction of a System for Experimental Mathematics. Calculemus/MKM 2007: 13-26 - [c15]William M. Farmer:
Biform Theories in Chiron. Calculemus/MKM 2007: 66-79 - 2006
- [p1]William M. Farmer:
IMPS. The Seventeen Provers of the World 2006: 72-87 - [e2]Jacques Carette, William M. Farmer:
Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2005, Newcastle-upon-Tyne, UK, July 18-19, 2005. Electronic Notes in Theoretical Computer Science 151(1), Elsevier 2006 [contents] - [e1]Jonathan M. Borwein, William M. Farmer:
Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings. Lecture Notes in Computer Science 4108, Springer 2006, ISBN 3-540-37104-4 [contents] - 2005
- [c14]Jacques Carette, William M. Farmer:
Preface. Calculemus 2005: 1-2 - 2004
- [j15]William M. Farmer:
MKM: a new interdisciplinary field of research. SIGSAM Bull. 38(2): 47-52 (2004) - [c13]William M. Farmer:
Formalizing Undefinedness Arising in Calculus. IJCAR 2004: 475-489 - 2003
- [j14]William M. Farmer, Martin von Mohrenschildt:
An Overview of a Formal Framework for Managing Mathematics. Ann. Math. Artif. Intell. 38(1-3): 165-191 (2003) - 2001
- [j13]William M. Farmer:
STMM: A Set Theory for Mechanized Mathematics. J. Autom. Reason. 26(3): 269-289 (2001) - 2000
- [j12]William M. Farmer, Joshua D. Guttman:
A Set Theory with Support for Partial Functions. Stud Logica 66(1): 59-78 (2000) - [c12]William M. Farmer:
An Infrastructure for Intertheory Reasoning. CADE 2000: 115-131
1990 – 1999
- 1999
- [c11]William M. Farmer:
A Scheme for Defining Partial Higher-Order Functions by Recursion. IWFM 1999 - 1996
- [c10]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
IMPS: An Updated System Description. CADE 1996: 298-302 - [c9]William M. Farmer, Joshua D. Guttman, Vipin Swarup:
Security for Mobile Agents: Authentication and State Appraisal. ESORICS 1996: 118-130 - [c8]William M. Farmer, Richard F. Freund, Mark Furtney, Paul Messina, Lionel M. Ni, Charles L. Seitz, Marc Snir:
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? IPPS 1996: 631-634 - 1995
- [j11]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
Context in Mathematical Reasoning and Computation. J. Symb. Comput. 19(1-3): 210-206 (1995) - 1994
- [c7]William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer:
Proof Script Pragmatics in IMPS. CADE 1994: 356-370 - 1993
- [j10]William M. Farmer:
A Simple Type Theory with Partial Functions and Subtypes. Ann. Pure Appl. Log. 64(3): 211-240 (1993) - [j9]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
IMPS: An Interactive Mathematical Proof System. J. Autom. Reason. 11(2): 213-248 (1993) - [c6]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
Reasoning with Contexts. DISCO 1993: 216-228 - [c5]William M. Farmer:
Theory Interpretation in Simple Type Theory. HOA 1993: 96-123 - 1992
- [j8]William M. Farmer:
The Kreisel Length-of-Proof Problem. Ann. Math. Artif. Intell. 6(1-3): 27-55 (1992) - [c4]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
Little Theories. CADE 1992: 567-581 - [c3]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
IMPS: System Description. CADE 1992: 701-705 - 1991
- [j7]William M. Farmer:
A Unification-Theoretic Method for Investigating the k-Provability Problem. Ann. Pure Appl. Log. 51(3): 173-214 (1991) - [j6]William M. Farmer:
Simple Second-order Languages for which Unification is Undecidable. Theor. Comput. Sci. 87(1): 25-41 (1991) - [c2]William M. Farmer, Ronald J. Watro:
Redex Capturing in Term Graph Rewriting (Concise Version). RTA 1991: 13-24 - 1990
- [j5]William M. Farmer, Ronald J. Watro:
Redex Capturing in Term Graph Rewriting. Int. J. Found. Comput. Sci. 1(4): 369-386 (1990) - [j4]William M. Farmer:
A Partial Functions Version of Church's Simple Theory of Types. J. Symb. Log. 55(3): 1269-1291 (1990) - [j3]William M. Farmer, John D. Ramsdell, Ronald J. Watro:
A Correctness Proof for Combinator Reduction with Cycles. ACM Trans. Program. Lang. Syst. 12(1): 123-134 (1990) - [c1]William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
IMPS: An Interactive Mathematical Proof System. CADE 1990: 653-654
1980 – 1989
- 1989
- [j2]William M. Farmer, A. J. Kfoury:
Minutes of the 4th annual LICS business meeting. SIGACT News 20(4): 43-47 (1989) - 1988
- [j1]William M. Farmer:
A unification algorithm for second-order monadic terms. Ann. Pure Appl. Log. 39(2): 131-174 (1988)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-18 20:44 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
