| 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.
|
| References: |
|
| Organizer's note: | Please bring your lunch.
|