Tags:amortised cost analysis, automation, constraint solving, functional programming, probabilistic programming and self-adjusting data structures
Abstract:
In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps and randomised meldable heaps, which so far have only (semi-)manually been analysed in the literature. We generalise a recently proposed type-and-effect system for logarithmic amortised resource analysis, proposed by Hofmann et al. to probabilistic programs. Further, we provide a prototype implementation able to fully automatically analyse the aforementioned case studies.
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures