SWS   Info

Public Audience

English

60 Minutes

Saarbrücken

Amortized analysis is a standard algorithmic technique for estimating upper bounds on the average costs of functions, specifically operations on data structures. This thesis intends to develop λ-amor, a type-theory for amortized analysis of higher-order functional programs. A typical amortized analysis works by storing ghost resource called /potential/ with a data structure's internal state. Accordingly, the central idea in λ-amor is a type-theoretic construct to associate potential with an arbitrary type. Additionally, λ-amor relies on standard concepts from substructural and modal type systems: indexed monads, affine types and indexed exponential types. We show that λ-amor is not only sound (in a very elementary logical relations model), but also very expressive: It can be used to analyze both eager and lazy data structures, and it can embed existing resource analysis frameworks. In fact, λ-amor is /complete/ for the cost analysis of lazy PCF programs. Further, the basic principles behind λ-amor can be adapted (by dropping affineness and adding mutable state) to obtain an expressive type system for a completely unrelated application, namely, information flow control.

The proposal talk will cover the broad setting and the motivation of the work and a significant subset of λ-amor, but due to time constraints, it will not cover all of λ-amor or the adaptation to information flow control. Implementation of the two type theories is not in the scope of the thesis.

--email hidden

Yes

Kaiserslautern

G26

111

SWS Space 2 (6312)

passcode not visible

logged in users only