Formalization of O Notation in Isabelle/HOL

Abstract

We are working on formalizing a proof of the prime number theorem using Isabelle/HOL. In support of this project we formalized a very general notion of O notation.

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

My notes

Similar books and articles

Formalizing O notation in isabelle/hol.Jeremy Avigad - manuscript
Notes on a formalization of the prime number theorem.Jeremy Avigad - unknown
Formalised cut admissibility for display logic.Rajeev Gore - manuscript
Formalised Cut Admissibility for Display Logic.Jeremy E. Dawson - unknown
A Formally Verified Proof of the Prime Number Theorem.Jeremy Avigad, Kevin Donnelly, David Gray & Paul Raff - 2007 - ACM Transactions on Computational Logic 9 (1).
Writing the Present.Michael Sheringham - 2008 - Sign Systems Studies 36 (1):11-29.
Embedding display calculi into logical frameworks : Comparing twelf and Isabelle.Jeremy E. Dawson - unknown
Polymorphic type checking for the type theory of the Principia Mathematica of Russell and Whitehead.M. Randall Holmes - unknown
Review of Isabelle Stengers, Cosmopolitics I. [REVIEW]Jeff Kochan - 2011 - Isis 102 (3):594-595.
Tarskian semantics, or no notation without denotation.Drew McDermott - 1978 - Cognitive Science 2 (3):277-82.
Limitations of formalization.Constantine Politis - 1965 - Philosophy of Science 32 (3/4):356-360.
Ordinal diagrams for Π3-reflection.Toshiyasu Arai - 2000 - Journal of Symbolic Logic 65 (3):1375 - 1394.
Diagrammatic reasoning in Frege’s Begriffsschrift.Danielle Macbeth - 2012 - Synthese 186 (1):289-314.

Analytics

Added to PP
2010-12-22

Downloads
49 (#317,389)

6 months
2 (#1,232,442)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references