Guarantees for resource-bounded computations

Olha Sharavska

Institut für Informatik
Ludwig-Maximilians-Universität München

Monday, 23 May 2005, 14:00 (note the unusual weekday!)
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: We outline a Mobile Resource Guarantees framework, which ensures that downloaded functional programs are free from run-time violations of resource bounds.

The resource constraints are encoded in the type system of a novel functional language Camelot. The type system streamlines the generation of a proof of resource bounds for a given program. The proof is attached to the source code and plays a role of a certificate.

In this talk we will focus on technical aspects of automatic translation from high-level typing derivations into low-level program logic assertions.

Tarmo Uustalu
Last update 25.5.2005