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.Links
PhilArchive
External links
(no proxy)
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
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: Notation in Barthes’s Collège de France lectures.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
Tarskian semantics, or no notation without denotation.Drew McDermott - 1978 - Cognitive Science 2 (3):277-82.
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
47 (#251,310)
6 months
1 (#451,398)
2010-12-22
Downloads
47 (#251,310)
6 months
1 (#451,398)
Historical graph of downloads
