Research activity in 2001
The interest of our group focuses mainly on the study of 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 2001 has been mainly focused on the study of filter models, and their relations with intersection types and with the behaviours of lambda terms, moreover it has concerned studies involving sub-linear logics related to subtyping.
In [ADH01] we illustrate the use of intersection types as a tool for synthesizing lambda-models which exhibit special purpose features. We focus on semantical proofs of easiness. This allows us to prove that the class of lambda-theories induced by graph models is strictly included in the class of lambda-theories induced by non-extensional filter models.
In [BT01] a logical semantics for a polymorphic subtyping relation enriched with a cartesian product type constructor is presented. This work extends some previous research by Jerzy Tiuryn about modelling subtyping relations via sub-linear logics. In the paper, a sound and complete axiomatization of the enriched subtyping is presented, together with a proof of non-encodability of the product axioms in the pure polymorphic system. The logical semantics is based on a special sequent form where the right-hand side is a tree of judgements. From this sequent form, a calculus a` la` Gentzen and a natural deduction are developed.
[DGh01] builds a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms.
There are essentially two ways of looking at the computational behaviours of lambda-terms. One consists in putting the term within a context (possibly of lambda -calculus extensions) and observing some properties (typically termination). The other consists in reducing the term until some meaningful information is obtained: this naturally leads to a tree representation of the information implicitly contained in the original term. [DGh01] is an informal overview of the role played by Boehm's Theorem in these observations of terms.
In [DHM01] we prove that many intersection type theories of interest (including those which induce as filter models, Scott's and Park's models, the models studied in Barendregt Coppo Dezani, Abramsky Ong, and Honsell Ronchi) satisfy an Approximation Theorem with respect to a suitable notion of approximant.
This theorem implies that a lambda-term has a type if and only if there exists an approximant of that term which has that type. We prove this result uniformly for all the intersection type theories under consideration using a Kripke version of stable sets where bases correspond to worlds.
In [MMB01] a classical logic-based semantics for B+ (the positive minimal relevant logic) is presented. In this perspective, the relevant provability is translated by the classical validity, through CB, that is a conservative boolean extension of B+.
Inside the Project "TOSCA" the research activity in the year 2001 has been mainly focused on the study of class based languages and mobile ambients.
A research topic is concerned about relationships between the object-oriented programming paradigm and the data types as algebras approach in functional programming. Boehm's CuCh machine extends the pure lambda--calculus with algebraic data types and provides the possibility of defining functions over disjoint sums of algebras. In [BS01], such natural form of overloading is exploited to define a functional interpretation of a simple, but significant fragment of a typical object--oriented class--based language.
Reclassification changes at run-time the class membership of an object while retaining its identity. In [DDDG01a] and [DDDG01b] we suggest language features for object reclassification, which could extend an imperative, typed, class-based, object-oriented language. We present our proposal through the language Fickle. The imperative features combined with the requirement for a static and safe type system provided the main challenges. We develop a type and effect system for Fickle and prove its soundness with respect to the operational semantics. In particular, even though objects may be re-classified across classes with different members, they will never attempt to access non-existing members.
In [VS01] a distributed abstract machine for the ambient calculus is presented, and proved operationally correct. This abstract machine is different from previous implementations of ambient-like calculi, mainly because the underlying calculus is typed safe ambients rather than the untyped ambient calculus; moreover in our paper we separate the logical structure of ambient systems from their physical distribution. In this work we also discuss a prototype implementation of our abstract machine, written in Java and designed after the interpreter pattern.
