Seminar: Formalizing Syntax-Based Mathematical Algorithms: Challenges and Approaches by Dr. William M. Farmer

Guest Speaker: William M. Farmer, Professor, McMaster University

William M. Farmer is a Professor in the Department of Computing and Software at McMaster University. He received a B.A. in mathematics from the University of Notre Dame in 1978. He attended graduate school at the University of Wisconsin-Madison, where he received a M.A. in mathematics in 1980, a M.S. in computer sciences in 1983, and a Ph.D. in mathematics in 1984. Before joining McMaster in 1999, he conducted research in various areas of computer science for twelve years at the MITRE Corporation in Bedford, Massachusetts and taught computer programming and networking courses for two years at St. Cloud State University in St. Cloud, Minnesota.

Dr. Farmer's research interests are applied logic, mechanized mathematics, practice-oriented logics, mathematical knowledge management, and rigorous methods of software development. One of his most significant achievements is the design and implementation of the IMPS Interactive Mathematical Proof System, wich was done at MITRE in partnership with Dr. Joshua Guttman and Dr. Javier Thayer. He and Dr. Jacques Carette are currently leading the MathSceme project whose goal is to develop a new approach to mechanized mathematics in which axiomatic and algorithmic mathematics are tightly integrated.

Abstract:

A syntax-based mathematical algorithm (SBMA) is an algorithm that manipulates the syntax of mathematical expressions in a mathematically meaningful way. Examples include algorithms tat apply arithmetic operations to numerals, factor polynomials, invert matrices, and symbolically differentiate functional expressions. Formalizing an SBMA -- defining or specifying its computational behaviour, proving theorems about its mathematical meaning, and applying it to formal mathematical expressions -- requires the ability to reason about the interplay of syntax and semantics that is embodied in the algorithm. Traditional logics like first-order logic and simple type theory provide little support for this kind of reasoning. In this talk, we will give an overview of the challenges and approaches that are involved in incorporating SBMAs into proof assistants and libraries of formal mathematics. We will also outline our work on developing a traditional-style logic with global quotation and evaluation operators (a la Lisp) that is well suited for formalizing SBMAs.