William M. Farmer

80 papers A 8B 1C 8Misc 1Journal 37Unranked 16

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility. CoRR William M. Farmer
2025	—	`book`	Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas, Second Editiontion William M. Farmer
2023	J	`jnl`	Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory. CoRR William M. Farmer, Dennis Y. Zvigelsky
2023	—	`book`	Simple Type Theory - A Practical Logic for Expressing and Reasoning About Mathematical Ideas William M. Farmer
2021	—	`conf`	Formal Mathematics for the Masses (short paper). CICM Workshops William M. Farmer
2020	—	`ed.`	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. CICM Workshops Edwin C. Brady, James H. Davenport, William M. Farmer, Cezary Kaliszyk, Andrea Kohlhase, Michael Kohlhase, Dennis Müller, Karol Pak, Claudio Sacerdoti Coen
2020	C	`conf`	Leveraging the Information Contained in Theory Presentations. CICM Jacques Carette, William M. Farmer, Yasmine Sharoda
2020	J	`jnl`	Leveraging the Information Contained in Theory Presentations. CoRR Jacques Carette, William M. Farmer, Yasmine Sharoda
2020	J	`jnl`	The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. CoRR Katja Bercic, Jacques Carette, William M. Farmer, Michael Kohlhase, Dennis Müller, Florian Rabe, Yasmine Sharoda
2019	J	`jnl`	Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal. CoRR Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe
2019	—	`ed.`	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. CICM Workshops 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
2019	C	`conf`	Towards Specifying Symbolic Computation. CICM Jacques Carette, William M. Farmer
2019	J	`jnl`	Towards Specifying Symbolic Computation. CoRR Jacques Carette, William M. Farmer
2018	—	`conf`	A New Style of Mathematical Proof. ICMS William M. Farmer
2018	J	`jnl`	A New Style of Mathematical Proof. CoRR William M. Farmer
2018	C	`conf`	Biform Theories: Project Description. CICM Jacques Carette, William M. Farmer, Yasmine Sharoda
2018	J	`jnl`	Biform Theories: Project Description. CoRR Jacques Carette, William M. Farmer, Yasmine Sharoda
2018	B	`conf`	HOL Light QE. ITP Jacques Carette, William M. Farmer, Patrick Laskowski
2018	J	`jnl`	HOL Light QE. CoRR Jacques Carette, William M. Farmer, Patrick Laskowski
2018	J	`jnl`	Incorporating quotation and evaluation into Church's type theory. Inf. Comput. William M. Farmer
2018	C	`ed.`	Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings CICM Florian Rabe, William M. Farmer, Grant O. Passmore, Abdou Youssef
2017	C	`conf`	Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. CICM Jacques Carette, William M. Farmer
2017	J	`jnl`	Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. CoRR Jacques Carette, William M. Farmer
2017	C	`conf`	Theory Morphisms in Church's Type Theory with Quotation and Evaluation. CICM William M. Farmer
2017	J	`jnl`	Theory Morphisms in Church's Type Theory with Quotation and Evaluation. CoRR William M. Farmer
2016	Misc	`conf`	A Formal Language for Writing Contracts. IRI William M. Farmer, Qian Hu
2016	J	`jnl`	Incorporating Quotation and Evaluation Into Church's Type Theory. CoRR William M. Farmer
2016	C	`conf`	Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics. CICM William M. Farmer
2016	J	`jnl`	Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics. CoRR William M. Farmer
2014	J	`jnl`	Andrews' Type Theory with Undefinedness. CoRR William M. Farmer
2014	—	`conf`	Meaning Formulas for Syntax-Based Mathematical Algorithms. SCSS William M. Farmer
2014	C	`conf`	Realms: A Structure for Consolidating Knowledge about Mathematical Theories. CICM Jacques Carette, William M. Farmer, Michael Kohlhase
2014	J	`jnl`	Realms: A Structure for Consolidating Knowledge about Mathematical Theories. CoRR Jacques Carette, William M. Farmer, Michael Kohlhase
2014	J	`jnl`	Simple Type Theory with Undefinedness, Quotation, and Evaluation. CoRR William M. Farmer
2013	J	`jnl`	Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation CoRR William M. Farmer
2013	J	`jnl`	Frameworks for Reasoning about Syntax that Utilize Quotation and Evaluation. CoRR William M. Farmer, Pouya Larjani
2013	J	`jnl`	The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation CoRR William M. Farmer
2013	—	`conf`	The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. MKM/Calculemus/DML William M. Farmer
2011	—	`ed.`	Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings Calculemus/MKM James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe
2011	—	`conf`	MathScheme: Project Description. Calculemus/MKM Jacques Carette, William M. Farmer, Russell O'Connor
2011	—	`ch.`	Mathematical Knowledge Management. Encyclopedia of Knowledge Management William M. Farmer
2011	J	`jnl`	The MathScheme Library: Some Preliminary Experiments CoRR Jacques Carette, William M. Farmer, Filip Jeremic, Vincent Maccio, Russell O'Connor, Quang M. Tran
2009	—	`conf`	A Review of Mathematical Knowledge Management. Calculemus/MKM Jacques Carette, William M. Farmer
2008	—	`conf`	High-Level Theories. AISC/MKM/Calculemus Jacques Carette, William M. Farmer
2008	—	`conf`	Panoptes: An Exploration Tool for Formal Proofs. UITP@TPHOLs William M. Farmer, Orlin G. Grigorov
2008	J	`jnl`	The seven virtues of simple type theory. J. Appl. Log. William M. Farmer
2007	—	`conf`	A Rational Reconstruction of a System for Experimental Mathematics. Calculemus/MKM Jacques Carette, William M. Farmer, Volker Sorge
2007	—	`conf`	Biform Theories in Chiron. Calculemus/MKM William M. Farmer
2006	—	`ch.`	IMPS. The Seventeen Provers of the World William M. Farmer
2006	—	`ed.`	Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings MKM Jonathan M. Borwein, William M. Farmer
2006	—	`ed.`	Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2005, Newcastle-upon-Tyne, UK, July 18-19, 2005 Calculemus Jacques Carette, William M. Farmer
2005	—	`conf`	Preface. Calculemus Jacques Carette, William M. Farmer
2004	A	`conf`	Formalizing Undefinedness Arising in Calculus. IJCAR William M. Farmer
2004	J	`jnl`	MKM: a new interdisciplinary field of research. SIGSAM Bull. William M. Farmer
2003	J	`jnl`	An Overview of a Formal Framework for Managing Mathematics. Ann. Math. Artif. Intell. William M. Farmer, Martin von Mohrenschildt
2001	J	`jnl`	STMM: A Set Theory for Mechanized Mathematics. J. Autom. Reason. William M. Farmer
2000	J	`jnl`	A Set Theory with Support for Partial Functions. Stud Logica William M. Farmer, Joshua D. Guttman
2000	A	`conf`	An Infrastructure for Intertheory Reasoning. CADE William M. Farmer
1999	—	`conf`	A Scheme for Defining Partial Higher-Order Functions by Recursion. IWFM William M. Farmer
1996	—	`conf`	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 William M. Farmer, Richard F. Freund, Mark Furtney, Paul Messina, Lionel M. Ni, Charles L. Seitz, Marc Snir
1996	A	`conf`	IMPS: An Updated System Description. CADE William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1996	A	`conf`	Security for Mobile Agents: Authentication and State Appraisal. ESORICS William M. Farmer, Joshua D. Guttman, Vipin Swarup
1995	J	`jnl`	Context in Mathematical Reasoning and Computation. J. Symb. Comput. William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1994	A	`conf`	Proof Script Pragmatics in IMPS. CADE William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer
1993	J	`jnl`	A Simple Type Theory with Partial Functions and Subtypes. Ann. Pure Appl. Log. William M. Farmer
1993	J	`jnl`	IMPS: An Interactive Mathematical Proof System. J. Autom. Reason. William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1993	—	`conf`	Reasoning with Contexts. DISCO William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1993	—	`conf`	Theory Interpretation in Simple Type Theory. HOA William M. Farmer
1992	A	`conf`	IMPS: System Description. CADE William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1992	A	`conf`	Little Theories. CADE William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1992	J	`jnl`	The Kreisel Length-of-Proof Problem. Ann. Math. Artif. Intell. William M. Farmer
1991	J	`jnl`	A Unification-Theoretic Method for Investigating the k-Provability Problem. Ann. Pure Appl. Log. William M. Farmer
1991	—	`conf`	Redex Capturing in Term Graph Rewriting (Concise Version). RTA William M. Farmer, Ronald J. Watro
1991	J	`jnl`	Simple Second-order Languages for which Unification is Undecidable. Theor. Comput. Sci. William M. Farmer
1990	J	`jnl`	A Correctness Proof for Combinator Reduction with Cycles. ACM Trans. Program. Lang. Syst. William M. Farmer, John D. Ramsdell, Ronald J. Watro
1990	J	`jnl`	A Partial Functions Version of Church's Simple Theory of Types. J. Symb. Log. William M. Farmer
1990	A	`conf`	IMPS: An Interactive Mathematical Proof System. CADE William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1990	J	`jnl`	Redex Capturing in Term Graph Rewriting. Int. J. Found. Comput. Sci. William M. Farmer, Ronald J. Watro
1989	J	`jnl`	Minutes of the 4th annual LICS business meeting. SIGACT News William M. Farmer, A. J. Kfoury
1988	J	`jnl`	A unification algorithm for second-order monadic terms. Ann. Pure Appl. Log. William M. Farmer