Time:  12  1:20 p.m. 
Room: 
CFA 110

Speaker:  Kevin Donnelly Undergraduate Student in Computer Science Carnegie Mellon University 
Title: 
Formalization of BigO 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 BigO notation in this system. In this
talk I will discuss Isabelle's type theory and our formalization of BigO
notation in it, as well as showing some examples of its use in number
theory towards a proof of the PNT.

References: 

Organizer's note:  Please bring your lunch.
