We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Type-Based Analysis of Logarithmic Amortised Complexity

Abstract: We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis, and is potential-based. The type system makes use of logarithmic potential functions and is the first such system to exhibit *logarithmic amortised complexity*. With our approach we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of *splaying*, once the type annotations are fixed.
Comments: 35 pages. arXiv admin note: text overlap with arXiv:1807.08242
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
ACM classes: F.3.2
Cite as: arXiv:2101.12029 [cs.LO]
  (or arXiv:2101.12029v2 [cs.LO] for this version)

Submission history

From: Georg Moser [view email]
[v1] Thu, 28 Jan 2021 14:47:45 GMT (112kb,D)
[v2] Sun, 31 Jan 2021 17:45:07 GMT (132kb,D)

Link back to: arXiv, form interface, contact.