Principles of Programming Seminar

— 4:00pm

Location:
In Person - Reddy Conference Room, Gates Hillman 4405

Speaker:
GEORG MOSER, Full Professor of Theoretical Computer Science, Department of Computer Science, Universität Innsbruck
https://tcs-informatik.uibk.ac.at/users/georg/

Automated Expected Cost Analysis of Splaying et al.

In this talk, I present recent work on fully-automated (expected) amortised cost analysis of self-adjusting data structures, like splay trees or splay heaps, as well as probabilistic data structures like randomised splay trees or splay heaps and randomised meldable heaps. Prior to our work, these data structures have only (semi-)manually been analysed in the literature. Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models. With our prototype implementation, we have been able automatically infer bounds on the (expected) amortised cost, which could previously only be obtained by sophisticated pen-and-paper proofs. In particular, we verify that the amortised costs of randomised variants of self-adjusting data structures improve upon their non-randomised variants.

This is joint work with Lorenz Leutgeb and Florian Zuleger.

—

Georg Moser is a Full Professor of Theoretical Computer Science at the University of Innsbruck since February 2020. He studied Computer Science and Logic at the Vienna University of Technology and the University of Leeds, respectively. Prior to his appointment to full professor, he has been an associate professor at the University ofInnsbruck, heading a research group on computation with bounded resources. His research interests center around logic and program analysis. For the latter, a recent focus of his work is on probabilistic programming and Quantum computation. He has lead a number of national and international research consortia. He has acted as steering committee chair and member of international conference series and similar research consortia and continues to do so. Moreover, he has been chair of the IFIP Working Group 1.6. His expertise is frequently sought as a program committee member of most prominent conferences such as FSCD, LICS, etc. Further, he has frequently provided editorial services.

Faculty Host: Jan Hoffman