LFCS Seminar: Tuesday 18th August: Georg Moser | LFCS

Title: Automated Amortised Analysis of Skew Heaps and Leftist Heaps

Abstract: We study the fully automated amortised analysis of purely functional

data structures like skew heaps, as well as weight- and rank-biased

leftist heaps. For that we generalise earlier works on automated

amortised resource analysis by developing a type inference based

approach with a generic type system. This allows for modular reasoning

and the inference of precise and optimal cost bounds.

More specifically, we extend the work on the ATLAS system by Leutgeb et

al. which was developed to cover the analysis of splay trees and some

closely related data structures. To enable the analysis of skew heaps,

however, and the even more challenging (amortised) analysis of

leftist heaps, we have developed a range of new techniques for

type-based automated analysis. By introducing a generic type system

we allow for arbitrary (classes of) potential functions, compared to

the use of hard-coded potential functions in ATLAS, which we have

implemented in Haskell in an entirely modular way. We have also greatly

enhanced the existing type inference algorithm by extensions in

multiple directions, including path-sensitive reasoning, data

structure invariants, and template parameters for piecewise defined

potential functions. We show how our newly developed system supports

the use of all known potential functions for analysing skew heaps and

leftist heaps, confirming the known bounds.

Joint work with Armin Walch, Berry Schoenmakers, and Florian Zuleger.

This article was published on Friday 14 August 2026