Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:A type theory for amortized resource analysis
Speaker:Vineet Rajani
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Proposal
Visibility:SWS
We use this to send out email in the morning.
Level:Public Audience
Language:English
Date, Time and Location
Date:Tuesday, 27 August 2019
Time:14:00
Duration:60 Minutes
Location:Saarbrücken
Building:E1 5
Room:029
Abstract
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.

Contact
Name(s):
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:SWS Space 2 (6312)
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
  • Maria-Louise Albrecht, 07/25/2019 04:30 PM
  • Maria-Louise Albrecht, 07/25/2019 04:18 PM -- Created document.