[PL Seminar] Talk: Markus Degen
2009.09.11 |
| Date | Wed Sep 16 |
| Time | 15:30 — 16:30 |
| Location | DI-Turing-014 |
Title: Tracking Linear and Affine Resources with Java(X)
Speaker: Markus Degen, Albert-Ludwigs-Universität Freiburg
Time and place: 16.9.09, 15:30-16:15 in Turing-014.
Abstract:
Java(X) is a framework for type refinement. It extends Java’s type
language with annotations drawn from an algebra X and structural
subtyping in terms of the annotations. Each instantiation of X yields a
different refinement type system with guaranteed soundness. The paper
presents some applications, formalizes a core language, states a generic
type soundness result, and sketches the extensions required for the full
Java language (without generics).
The main technical innovation of Java(X) is its concept of activity
annotations paired with the notion of droppability. An activity
annotation is a capability which can grant exclusive write permission
for a fieldin an object and thus facilitates a typestate change (strong
update). Propagation of capabilities is either linear or affine (if they
are droppable). Thus, Java(X) can perform protocol checking as well as
refinement typing. Aliasing is addressed with a novel splitting relation
on types.