$title1="Seminariteade / Seminar announcement"; $papa="./"; include($_SERVER['DOCUMENT_ROOT']."/head.html.en"); ?>
Speaker: | Olha SHKARAVSKA, Institut für Informatik, Ludwig-Maximilians-Universität München |
Place: | Room B101, Cybernetica Bldg, Akadeemia tee 21, Tallinn, Estonia |
Time: | Monday, May 23, 2005, 14:00 |
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.