Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

Reminding that the LFCS seminar will start shortly:

  Tuesday, 18 Aug, 4.10pm

  Georg Moser, University of Innsbruck

  The seminar will take place in-person only.

We're synchronising the seminar time with the teaching timetable, and

plan to start the talk at the advertised time, so please arrive a minute or two

earlier.

In detail:

----------------------------------------------------------------------

Georg Moser, University of Innsbruck

https://www.uibk.ac.at/en/theoretical-computer-science/

  Tue, 18 Aug, 4.10pm

  Venue: IF G.03

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.

----------------------------------------------------------------------

Upcoming events:

----------------

07 Sep: Gordon Plotkin's 80th birthday celebration

  https://events.inf.ed.ac.uk/plotkin80/

08 Sep: LFCS's 40th anniversary celebration

  https://events.inf.ed.ac.uk/lfcs40/

09 Sep: Philip Wadler's 70th birthday celebration

  https://events.inf.ed.ac.uk/wadler70/

Upcoming seminars:

------------------

15 Sep: Pranshu Gaba, Tata Institute of Fundamental Research, Mumbai

If you would like to propose a speaker, or speak yourself, please contact me.

The seminar webpages:

http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,

Ohad.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.