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: 93,990

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

Formalization of O Notation in Isabelle/HOL.Kevin Donnelly - unknown
Isabelle for Philosophers.Ben Blumson - manuscript
On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle/HOL as a case study.Thomas Bittner - 2019 - Applied ontology 14 (3):251-292.
Formalising Mathematics in Simple Type Theory.Lawrence Paulson - 2019 - In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer Verlag. pp. 437-453.
Formalised Cut Admissibility for Display Logic.Jeremy E. Dawson - unknown
Formalised cut admissibility for display logic.Rajeev Gore - manuscript
Ackermann’s function in iterative form: A proof assistant experiment.Lawrence C. Paulson - 2021 - Bulletin of Symbolic Logic 27 (4):426-435.
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.David Fuenmayor & Christoph Benzmüller - unknown
Anselm's God in Isabelle/HOL.Ben Blumson - 2017 - Archive of Formal Proofs:9.
Notes on a formalization of the prime number theorem.Jeremy Avigad - unknown

Analytics

Added to PP
2009-01-28

Downloads
74 (#218,182)

6 months
5 (#837,573)

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