Integrating Formal Proofs with Software using Dependent Type Theory
Russell O'Connor, McMaster University
Friday, January 22, 2010 at 11:30am
, at U. of Waterloo.
Abstract:
During the foundational crisis of mathematics in the early 20th century,
formal logic systems were developed to address what does and does not
constitute a valid deduction. These proof systems were so tedious that no one was expected to create formal deductions. Mathematical proofs are simply prose formal enough that they could, in theory, be translated into a formal deduction.
Today, modern digital computers excel at tedious tasks. This along with modern deductions systems have given us the ability to create completely formal mathematical proofs that are entirely checked by computer. These proofs are of the highest assurance available today.
My talk will describe how formalized mathematics, particularly formalized constructive mathematics, can be used to create mathematics and software of the highest reliability by integrating deduction and programming into one language: dependent type theory.
Russell O'Connor obtained a bachelor's degree in pure mathematics and computer science from the University of Waterloo. He was recently awarded a PhD 'cum laude' from Radboud University Nijmegen in the Foundations Group for his work on efficient computer verified exact real arithmetic. He now holds a post-doctoral position at McMaster University's department of Computing and Software working on the MathScheme system as part of the Software Certification project.
|