People

Research activity in 2000

The interest of our group focuses mainly on the study type systems for functional, concurrent and object-oriented languages. The theoretical basis is Curry type assignment system for pure lambda-calculus and its extensions.

Inside the Project "Fondamenti dei linguaggi funzionali" the research activity in the year 2000 has been mainly focused on the study of filter models, and their relations with intersection types and with the behaviours of lambda terms.

In [1] an unifying setting in which a generic type theory can be embedded is introduced and the conditions leading to filter lambda-models are investigated. As the order relation of type inclusion is essential for the definition of filters, the set of types is defined as any partial order having a largest element and closed for arrow type construction. The sets of types having an infimum are given by a collection Z of subsets of types, called subset system. For each choice of the subset system Z, a particular type theory is obtained; it is shown that some well-known type theories can be defined in terms of Z-type theories. In the case where the properties of the Z-subset system guarantees the existence of a filter-model, the proof of soundness and completeness of the associated type assignment is given and the set of representable functions is characterized.

The paper [2] shows how to characterize compositionally a number of evaluation properties of lambda-terms using Intersection Type assignment systems. In particular, this paper focus on termination properties, such as strong normalization, normalization, head normalization, and weak head normalization. It considers also the persistent versions of such notions, and, by way of example, it considers also another evaluation property, unrelated to termination, namely reducibility to a closed term. Many of these characterization results are new, or else they streamline, strengthen, or generalize earlier results in the literature. The completeness parts of the characterizations are proved uniformly for all the properties, using a set-theoretical semantics of intersection types over suitable kinds of stable sets. This technique generalizes Krivine's and Mitchell's methods for strong normalization to other evaluation properties.

Another contribution is an extension of lambda calculus for which the Berarducci trees equality coincides with observational equivalence, when one observes rootstable or rootactive behaviour of terms [4]. In one direction the proof is an adaptation of the classical Bohm-out technique. In the other direction the proof is based on confluence for strongly converging reductions in this extension.

In [5] we characterize those intersection-type theories which yield complete intersection-type assignment systems for lambda-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of the intersection constructor set-theoretic inclusion, and by taking the interpretation of the arrow constructor à la Scott, with respect to either any possible functionality set, or the largest one, or the least one. These results strengthen and generalize significantly all earlier results in the literature, to our knowledge, in at least three respects. First of all the inference semantics had not been considered before. Secondly, the characterizations are all given just in terms of simple closure conditions on the preorder relation on the types, rather than on the typing judgements themselves. The task of checking the condition is made therefore considerably more tractable. Lastly, we do not restrict attention just to lambda-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted lambda-calculi. Nevertheless the characterizations we give can be tailored just to the case of lambda-models.

An objective of our research inside the Project "Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi" has been a type discipline for safe mobile ambients [3]. The Ambient Calculus and the Safe Ambient Calculus have been recently successfully proposed as models for the Web. They are based on the notions of ambient movement and ambient opening. Different type disciplines have been devised for them in order to avoid unwanted behaviours of processes. The type discipline for safe mobile ambients of [3] is essentially motivated by ensuring security properties. We associate security levels to ambients and we require that an ambient at security levels can only be traversed or opened by ambients at security level at least s. Since the movement and opening right can be unrelated, we consider two partial orders between security levels.