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
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18820/
Grodin, Harrison ;
Harper, Robert
Amortized Analysis via Coinduction (Early Ideas)
Abstract
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
@InProceedings{grodin_et_al:LIPIcs.CALCO.2023.23,
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 = {https://drops.dagstuhl.de/opus/volltexte/2023/18820},
URN = {urn:nbn:de:0030-drops-188201},
doi = {10.4230/LIPIcs.CALCO.2023.23},
annote = {Keywords: amortized analysis, coinduction, data structure, mechanized proof}
}
