William Michael Farmer - McMaster Experts

Affiliations

Faculty of Engineering, McMaster University
Professor, Computing and Software, Faculty of Engineering

Scholarly Activity in McMaster Experts

Co-author Network

Scholarly Activity
Research
Teaching
Contact
View All

selected scholarly activity

books
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface. Ed. 6824 LNAI. 2011
chapters
- Mathematical Knowledge Management. 1082-1089. 2010
- Mathematical Knowledge Management. 599-604. 2006
conferences
- Formal Mathematics for the Masses. CEUR Workshop Proceedings. 2022
- Leveraging information contained in theory presentations. CEUR Workshop Proceedings. 2019
- Towards Specifying Symbolic Computation. Lecture Notes in Computer Science. 109-124. 2019
- A New Style of Mathematical Proof.. ICMS. 175-181. 2018
- Biform Theories: Project Description.. CICM. 76-86. 2018
- FCL: A Formal Language for Writing Contracts. Advances in Soft Computing. 190-208. 2018
- HOL Light QE.. ITP. 215-234. 2018
- Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study.. CICM. 9-24. 2017
- Theory Morphisms in Church’s Type Theory with Quotation and Evaluation. Lecture Notes in Computer Science. 147-162. 2017
- A Formal Language for Writing Contracts. 2016 IEEE 17th International Conference on Information Reuse and Integration (IRI). 134-141. 2016
- Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics.. CICM. 83-98. 2016
- Meaning Formulas for Syntax-Based Mathematical Algorithms.. SCSS. 10-11. 2014
- Realms: A Structure for Consolidating Knowledge about Mathematical Theories.. CICM. 252-266. 2014
- A Formalization of the C99 Standard in HOL, Isabelle and Coq.. Calculemus/MKM. 301-303. 2011
- A Foundational View on Integration Problems.. Calculemus/MKM. 107-122. 2011
- A Symbolic Companion for Interactive Geometric Systems.. Calculemus/MKM. 285-286. 2011
- A System for Computing and Reasoning in Algebraic Topology.. Calculemus/MKM. 295-297. 2011
- Combining Source, Content, Presentation, Narration, and Relational Representation.. Calculemus/MKM. 212-227. 2011
- Computer Certified Efficient Exact Reals in Coq.. Calculemus/MKM. 90-106. 2011
- Efficient Formal Verification of Bounds of Linear Programs.. Calculemus/MKM. 123-132. 2011
- Enumeration of AG-Groupoids.. Calculemus/MKM. 1-14. 2011
- Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.. Calculemus/MKM. 278-280. 2011
- Incidence Simplicial Matrices Formalized in Coq/SSReflect.. Calculemus/MKM. 30-44. 2011
- Indexing and Searching Mathematics in Digital Libraries - Architecture, Design and Scalability Issues.. Calculemus/MKM. 228-243. 2011
- Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings. Calculemus/MKM. 2011
- Interleaving Strategies.. Calculemus/MKM. 196-211. 2011
- Isabelle as Document-Oriented Proof Assistant.. Calculemus/MKM. 244-259. 2011
- Krextor - An Extensible Framework for Contributing Content Math to the Web of Data.. Calculemus/MKM. 304-306. 2011
- Large Formal Wikis: Issues and Solutions.. Calculemus/MKM. 133-148. 2011
- Learning2Reason.. Calculemus/MKM. 298-300. 2011
- Licensing the Mizar Mathematical Library.. Calculemus/MKM. 149-163. 2011
- MathScheme: Project Description. Lecture Notes in Computer Science. 287-288. 2011
- Parsing and Disambiguation of Symbolic Mathematics in the Naproche System.. Calculemus/MKM. 180-195. 2011
- Project Abstract: Logic Atlas and Integrator (LATIN).. Calculemus/MKM. 289-291. 2011
- Project EuDML - A First Year Demonstration.. Calculemus/MKM. 281-284. 2011
- Proof Assistant Decision Procedures for Formalizing Origami.. Calculemus/MKM. 45-57. 2011
- Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework.. Calculemus/MKM. 15-29. 2011
- System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org.. Calculemus/MKM. 307-309. 2011
- The LaTeXML Daemon: Editable Math on the Collaborative Web.. Calculemus/MKM. 292-294. 2011
- Towards Formal Proof Script Refactoring.. Calculemus/MKM. 260-275. 2011
- Using Theorema in the Formalization of Theoretical Economics.. Calculemus/MKM. 58-73. 2011
- View of Computer Algebra Data from Coq.. Calculemus/MKM. 74-89. 2011
- Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics.. Calculemus/MKM. 164-179. 2011
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library.. Calculemus/MKM. 276-277. 2011
- A Review of Mathematical Knowledge Management. Lecture Notes in Computer Science. 233-246. 2009
- High-Level Theories. Lecture Notes in Computer Science. 232-245. 2008
- A Rational Reconstruction of a System for Experimental Mathematics. Lecture Notes in Computer Science. 13-26. 2007
- Biform Theories in Chiron. Lecture Notes in Computer Science. 66-79. 2007
- A Dynamic Poincaré Principle.. MKM. 44-53. 2006
- A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus.. MKM. 67-81. 2006
- A Proof-Theoretic Approach to Tactics.. MKM. 54-66. 2006
- Authoring LeActiveMath Calculus Content.. MKM. 251-265. 2006
- Capturing Abstract Matrices from Paper.. MKM. 124-138. 2006
- Capturing the Content of Physics: Systems, Observables, and Experiments.. MKM. 165-178. 2006
- Communities of Practice in MKM: An Extensional Model.. MKM. 179-193. 2006
- From Notation to Semantics: There and Back Again.. MKM. 194-207. 2006
- From Untyped to Polymorphically Typed Objects in Mathematical Web Services.. MKM. 222-236. 2006
- IMPS. Lecture Notes in Computer Science. 72-87. 2006
- Information Retrieval and Rendering with.. MKM. 266-279. 2006
- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories.. MKM. 280-294. 2006
- Interpretation of Locales in Isabelle: Theories and Proof Contexts.. MKM. 31-43. 2006
- Managing Automatically Formed Mathematical Theories.. MKM. 237-250. 2006
- Managing Informal Mathematical Knowledge: Techniques from Informal Logic.. MKM. 208-221. 2006
- Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings. MKM. 2006
- Proof Transformation by CERES.. MKM. 82-93. 2006
- Roles of Math Search in Mathematics.. MKM. 2-16. 2006
- Stochastic Modelling of Scientific Terms Distribution in Publications.. MKM. 152-164. 2006
- Structured Induction Proofs in Isabelle/Isar.. MKM. 17-30. 2006
- Synthesizing Proof Planning Methods and Omega-Ants Agents from Mathematical Knowledge.. MKM. 94-109. 2006
- The Omega Number: Irreducible Complexity in Pure Math.. MKM. 1-1. 2006
- Towards a Parser for Mathematical Formula Recognition.. MKM. 139-151. 2006
- Verifying and Invalidating Textbook Proofs Using Scunak.. MKM. 110-123. 2006
- Simple type theory: simple steps towards a formal specification. Proceedings - Frontiers in Education Conference, FIE. fic-1-fic-6. 2004
- Formalizing Undefinedness Arising in Calculus. Lecture Notes in Computer Science. 475-489. 2004
- An Infrastructure for Intertheory Reasoning. Lecture Notes in Computer Science. 115-131. 2000
- A Scheme for Defining Partial Higher-Order Functions by Recursion.. IWFM. 1999
- 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. 631-634. 1996
- IMPS: An updated system description. Lecture Notes in Computer Science. 298-302. 1996
- Security for mobile agents: Authentication and state appraisal. Lecture Notes in Computer Science. 118-130. 1996
- Contexts in Mathematical Reasoning and Computation. Journal of Symbolic Computation. 201-216. 1995
- Proof script pragmatics in IMPS. Lecture Notes in Computer Science. 356-370. 1994
- Theory interpretation in simple type theory. Lecture Notes in Computer Science. 96-123. 1994
- Reasoning with contexts. Lecture Notes in Computer Science. 216-228. 1993
- IMPS - SYSTEM DESCRIPTION. AUTOMATED DEDUCTION - CADE-11. 701-705. 1992
- LITTLE THEORIES. AUTOMATED DEDUCTION - CADE-11. 567-581. 1992
- REDEX CAPTURING IN TERM GRAPH REWRITING (CONCISE VERSION). REWRITING TECHNIQUES AND APPLICATIONS. 13-24. 1991
- IMPS : An interactive mathematical proof system. Lecture Notes in Computer Science. 653-654. 1990
- SOME RESULTS ON THE K-PROVABILITY PROBLEM. Journal of Symbolic Logic (JSL). 1003-1003. 1988
- AN ALGORITHM FOR THE UNIFICATION OF 2ND-ORDER MONADIC TERMS. Journal of Symbolic Logic (JSL). 841-842. 1986
- A new approach to Fourier analysis of randomly sampled data using linear regression technique.. ICASSP. 89-93. 1981
journal articles
- Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge. Mathematical Intelligencer. 43:78-87. 2021
- The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems 2020
- Leveraging the Information Contained in Theory Presentations. Lecture Notes in Computer Science. 12236 LNAI:55-70. 2020
- Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal 2019
- Incorporating quotation and evaluation into Church's type theory. Information and Computation. 260:9-50. 2018
- A New Style of Mathematical Proof. Lecture Notes in Computer Science. 10931:175-181. 2018
- Biform Theories: Project Description. Lecture Notes in Computer Science. 11006:76-86. 2018
- HOL Light QE. Lecture Notes in Computer Science. 10895:215-234. 2018
- Incorporating quotation and evaluation into Church's type theory.. Inf. Comput.. 260:9-50. 2018
- Theory Morphisms in Church's Type Theory with Quotation and Evaluation. CICM. 10383:7-162. 2017
- Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. Lecture Notes in Computer Science. 10383:9-24. 2017
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics. Lecture Notes in Computer Science. 9791:83-98. 2016
- Andrews' Type Theory with Undefinedness. CoRR. abs/1406.7492. 2014
- Simple Type Theory with Undefinedness, Quotation, and Evaluation. CoRR. abs/1406.6706. 2014
- Realms: A Structure for Consolidating Knowledge about Mathematical Theories. Lecture Notes in Computer Science. 8543:252-266. 2014
- Frameworks for Reasoning about Syntax that Utilize Quotation and Evaluation. CoRR. abs/1308.2149. 2013
- Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation. CoRR. abs/1305.6206. 2013
- The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. CoRR. abs/1305.6052. 2013
- The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation. Lecture Notes in Computer Science. 7961 LNAI:35-50. 2013
- The MathScheme Library: Some Preliminary Experiments. CoRR. abs/1106.1862. 2011
- PREFACE. International Journal of Theoretical & Applied Finance. 14:v-vi. 2011
- Panoptes. Electronic Notes in Theoretical Computer Science. 226:39-48. 2009
- The seven virtues of simple type theory. Journal of Applied Logic. 6:267-286. 2008
- MKM. ACM SIGSAM Bulletin. 38:47-52. 2004
- An overview of a formal framework for managing mathematics. Annals of Mathematics and Artificial Intelligence. 38:165-191. 2003
- STMM: A set theory for mechanized mathematics. Journal of Automated Reasoning. 26:269-289. 2001
- A Set Theory with Support for Partial Functions. Studia Logica. 66:59-78. 2000
- Reasoning about partial functions with the aid of a computer. Erkenntnis: An International Journal of Scientific Philosophy. 43:279-294. 1995
- A simple type theory with partial functions and subtypes11Supported by the MITRE-Sponsored Research program. Presented at the 9th International Congress of Logic, Methodology and Philosophy of Science held in Uppsala, Sweden, August 7-14, 1991.. Annals of Pure and Applied Logic. 64:211-240. 1993
- IMPS: An interactive mathematical proof system. Journal of Automated Reasoning. 11:213-248. 1993
- The Kreisel length-of-proof problem. Annals of Mathematics and Artificial Intelligence. 6:27-55. 1992
- IMPS: System description. Lecture Notes in Computer Science. 607:701-705. 1992
- Little theories. Lecture Notes in Computer Science. 607:567-581. 1992
- Simple second-order languages for which unification is undecidable. Theoretical Computer Science. 87:25-41. 1991
- A unification-theoretic method for investigating the k-provability problem. Annals of Pure and Applied Logic. 51:173-214. 1991
- Redex capturing in term graph rewriting (concise version). Lecture Notes in Computer Science. 488:13-24. 1991
- REDEX CAPTURING IN TERM GRAPH REWRITING. International Journal of Foundations of Computer Science. 01:369-386. 1990
- A partial functions version of Church's simple theory of types. Journal of Symbolic Logic (JSL). 55:1269-1291. 1990
- A correctness proof for combinator reduction with cycles. ACM Transactions on Programming Languages and Systems. 12:123-134. 1990
- Minutes of the 4th annual LICS business meeting. ACM SIGACT News. 20:43-47. 1989
- A unification algorithm for second-order monadic terms. Annals of Pure and Applied Logic. 39:131-174. 1988
preprints