Teaching plan

The steady increase in expressiveness of type systems tends to clutter code with an excessive amount of type information which calls for the use of type inference. Several people have argued that a type inference should infer the best types possible within the given type discipline. We systematically construct such an inference for the Hindley-Milner type system by recasting type inference as a program analysis problem: We apply abstract interpretation theory to a denotational semantics and obtain typing rules that are correct by construction and abstract-complete in that they infer the best types. The resulting rules are a variant of Henglein's semi-unification--based inference rules. The notion of ``abstract complete'' is weaker than ``principal typings'' but we argue that the former delivers the same advantages and that the latter is not type system-agnostic.

We then observe that the Hindley-Milner type system is modular and reduce this fact to three properties developed in the abstract interpretation literature, namely, complete transfer functions, a complete projection operation and a condensing domain. Given the state-of-the-art, only two abstract domains feature these properties while remaining tractable, namely Herbrand abstractions and Boolean functions. We conclude that any modular type inference that infers principal typings must be based on these two domains. 

We might have an invited talk from the FCT 2011 conference that is organized at IFI from 22 to 25 August. 

In modeling a concurrent system, fairness constraints are usually considered at a specific granularity level of the system, leading to many different variants of fairness: transition fairness, object/process fairness, actor fairness, etc. These different notions of fairness can be unified by making explicit their parametrization over the relevant entities in the system as universal quantification. We propose a state/event-based framework as well as an on-the-fly model checking algorithm to verify LTL properties under universally quantified parametric fairness assumptions, specified by generalized strong/weak fairness formulas. It enables verification of temporal properties under fairness conditions associated to dynamic entities such as new process creations. We have implemented our algorithm within the Maude system. 

paper 

Reclassification changes the class membership of an object at run-time while retaining its identity. This presentation introduces a language with features for object reclassification. The approach is presented through the language FickleII which extends an imperative, typed, class-based, object-oriented language, where objects may be reclassified across classes with different members, so there will never be an attempt to access nonexisting members.

Paper 

Important security concerns, such as access control and runtime monitoring can be conveniently implemented using aspect-oriented programming languages. While aspect-oriented programming supports the modular definition of such crosscutting concerns, most approaches to aspect-oriented programming fail, however, to improve, or even preserve, modular reasoning. The main problem is that aspects usually carry, through their pointcuts, explicit references to the base code. These dependencies make programs fragile and hard to reason about. In this talk, we discuss how to separate base code and aspects using Join Point Interfaces, which are contracts between aspects and base code. Base code can define pointcuts that expose selected join points through a Join Point Interface. Conversely, an aspect can offer to advise join points that provide a given Join Point Interface. Crucially, however, aspect themselves cannot contain pointcuts, and hence cannot refer to base code elements. In addition, we will discuss Closure Joinpoints, a mechanism that allows base code to explicitly announce events to aspects. We will discuss why many previous attempts to defining such a language construct fail, and how Closure Joinpoints integrate with Join Point Interfaces to yield a language construct with a clear semantics, avoiding unwanted surprises.

"In this paper, we develop simple models to study the performance of BitTorrent, a second generation peer-to-peer (P2P) application. We first present a simple fluid model and study the scalability, performance and efficiency of such a file-sharing mechanism. We then consider the built-in incentive mechanism of BitTorrent and study its effect on net-work performance. We also provide numerical results based on both simulations and real traces obtained from the Internet."

paper from SIGCOM 2004 by Dongyu Qiu and R. Srikant

In a short demo (based on our work-in-progress) I will illustrate how the Ott-tool [1] could make your life easier by

• simplifying type-setting semantic rules in LaTeX;

• giving a small degree of consistency checking to your rules;

• helping you to establish your first foot-hold in theorem proving-land (here: Coq).

[1]: http://www.cl.cam.ac.uk/~pes20/ott/