License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2023.23
URN: urn:nbn:de:0030-drops-188201
Go to the corresponding LIPIcs Volume Portal

Grodin, Harrison ; Harper, Robert

Amortized Analysis via Coinduction (Early Ideas)

LIPIcs-CALCO-2023-23.pdf (0.7 MB)


Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented inductively, in terms of finite sequences of operations. We give an alternative coinductive formulation and prove that it is equivalent to the standard inductive definition. We describe a classic amortized data structure, the batched queue, and outline a coinductive proof of its amortized efficiency in calf, a dependent type theory for cost analysis.

BibTeX - Entry

  author =	{Grodin, Harrison and Harper, Robert},
  title =	{{Amortized Analysis via Coinduction}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{23:1--23:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-188201},
  doi =		{10.4230/LIPIcs.CALCO.2023.23},
  annote =	{Keywords: amortized analysis, coinduction, data structure, mechanized proof}

Keywords: amortized analysis, coinduction, data structure, mechanized proof
Collection: 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Issue Date: 2023
Date of publication: 02.09.2023
Supplementary Material: Software (Source Code): archived at:

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI