Formalizing O notation in isabelle/hol

Abstract

We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.

Categories

Keywords

Reprint years

Links

PhilArchive



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

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

Ordinal diagrams for Π3-reflection.Toshiyasu Arai - 2000 - Journal of Symbolic Logic 65 (3):1375 - 1394.
Formalised cut admissibility for display logic.Rajeev Gore - manuscript
Formalised Cut Admissibility for Display Logic.Jeremy E. Dawson - unknown
Notes on a formalization of the prime number theorem.Jeremy Avigad - 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).
Embedding display calculi into logical frameworks : Comparing twelf and Isabelle.Jeremy E. Dawson - 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.
Formalization of O Notation in Isabelle/HOL.Kevin Donnelly - unknown

Analytics

Added to PP
2009-01-28

Downloads
73 (#220,898)

6 months
4 (#818,853)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jeremy Avigad
Carnegie Mellon University

Citations of this work

Add more citations

References found in this work

No references found.

Add more references