Ernest Schimmerling

Mathematical logic seminar - October 2, 2003

Time: 12 - 1:20 p.m.

Room: CFA 110

Speaker: Kevin Donnelly
Undergraduate Student in Computer Science
Carnegie Mellon University

Title: Formalization of Big-O Notation in Isabelle/HOL

Abstract: Asymptotic notation is a way of making mathematically precise the notion of one function approximating another. Although used extensively in computer science, especially algorithms, asymptotic notation is also useful for other fields of mathematics. Isabelle is a general theorem proving framework based on typed lambda calculus. As part of a project with Jeremy Avigad to produce a formal proof of the Prime Number Theorem in Isabelle/HOL, I have formalized Big-O notation in this system. In this talk I will discuss Isabelle's type theory and our formalization of Big-O notation in it, as well as showing some examples of its use in number theory towards a proof of the PNT.

Organizer's note:     Please bring your lunch.