Research activity in 1999
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 1999 has been mainly focused on:
- the design of powerful type systems for object-oriented programming languages with functional features;
- the characterisation by means of types of looping functional programs.
The growing interest for object calculi to model and integrate the most important object-oriented features, such as the modularity and the object state data protection (encapsulation), giving the basis for the design of new languages, is also (and in great extents) due to the research on type systems, which offer mechanisms to develop and verify such calculi. On the other hand, problems arising in devising type systems for objects have stimulated the study of concepts nowadays considered foundational in type theory, such as subtyping and type recursion. An important aspect, both for following the evolution of technology and for allowing a quick experimentation of new systems is the possibility of having fast prototyping mechanisms. In such direction, we investigated the notion of ''incomplete'' objects . By incomplete objects we mean objects that present only some of the features requested to the
final product, but that are still able to perform a certain set of operations if they are placed in the right contexts. We explored [3] a calculus of "incomplete" objects, i.e., partially working objects with an incomplete implementation of their interface. This calculus can be seen as a proposal in the direction
of rapid prototyping, and it fits well in the context of studying partially specified computations. We studied [7] a semantics by encoding an object-based calculus [2] in a pure functional setting, by using a higher-order lambda calculus with records and recursive types, with the aim of putting extensible objects (which can be used to model classes) in a unifying frame (the frame presented by Bruce-Cardelli-Pierce). Such a calculus is a variation of the Fisher-Honsell-Mitchell Lambda Calculus of Objects which enligths features of extensible objects and interactions among object types and some forms of subtyping. We presented [8] an imperative calculus, which is an extension of basic ML with records, where classes are the only primitive construct. The aim of this work is to explore the concept of "class" in a more theoretical sense, by using a simple core system while keeping in mind some good software engineering ideas. A first extension of the previously mentioned work is adding to such core system the "mixin" constructor [6]. A mixin is nothing else than a class parametrized on its superclass. This kind of parametrized inheritance looks like a promising alternative to multiple inheritance, and the presented calculus is still simple enough to be considered a core system.
As regards to the characterisation by means of types of looping functional programs, recent work on infinitary versions of the lambda calculus has shown that the infinite lambda calculus can be a useful tool to study the unsolvable terms of the classical lambda calculus. Working in the framework of the intersection type disciplines, we devised [1] a type assignment system such that two terms are equal in the infinite lambda calculus if and only if they can be assigned the same types in any basis. This result can be considered as a step towards the goal of giving a denotational semantics for the lambda calculus suitable to study the unsolvable terms.
An objective of our research inside the Project "Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi" has been the logical semantics of Milner's pi-calculus, a paradigmatic language for describing computations involving mobile processes. While operational semantic is a common tool for specifying the semantics in an elegant and formally satisfactory way, it is nevertheless desirable to devise domains matching the behavioral preorders induced by "must" testing or finer preorders based on various notions of bisimulation in which to interpret denotationally problematic constructs, like the private names (with static scope) of the pi-calculus. For this purpose, there is evidence that suitably structured types can prove useful by allowing to make a denotational model out of properties of process terms. An advantage of this approach is that types automatically provide a logic in which to prove program properties. We defined [4] a filter model for pi-calculus, and proved its full abstraction with respect to a "may" operational semantics. The model is introduced in the form of a type assignment system. Types are related by a preorder which mimics the operational behaviour of terms. A subject expansion theorem holds. Terms are interpreted as filters of types: this interpretation is compositional. The proof of full abstraction relies on a notion of realizability of types, and on the construction of terms, which test when an arbitrary term has a fixed type.
Another interesting contribution [5] we gave to the Project "Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi" is the study of the concurrent lambda-calculus. In view of the integration between functional and concurrent programming languages, we have considered the addition of parallel and non-deterministic features to the lazy lambda calculus. In particular, we gave a constructive answer to the problem of when a functional procedure can replace another one leaving unchanged the observable behaviour of a process which uses it. Their main result is that two pure lambda terms are observationally equivalent in the lazy concurrent lambda calculus if and only if they have the same Lévy-Longo trees.
1999 Publications
Journals
A. Berarducci and M. Dezani-Ciancaglini. Infinite lambda-calculus and types. Theoretical Computer Science, 212:29-75, 1999. [1]
V. Bono and M. Bugliesi. Matching for the Lambda Calculus of Objects. Theoretical Computer Science 212(1-2) 101-140, February 1999. [2]
V. Bono, M. Bugliesi, L. Liquori and M. Dezani- Ciancaglini. A Subtyping for Extensible, Incomplete Objects. Fundamenta Informaticae, 38(4) 325-364, June 1999. [3]
F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. A filter model for mobile processes. Mathematical Structures in Computer Science, 9(1):63-102, 1999. [4]
M. Dezani-Ciancaglini, J. Tiuryn, and P. Urzyczyn. Discrimination by Parallel Observers: the Algorithm. Information and Computation, 150(2):153-186, 1999. [5]
Lecture Notes in Computer Science
V. Bono, A.J. Patel, V. Shmatikov. A Core Calculus of Classes and Mixins. In Proceedings European Conference on Object Oriented Programming (ECOOP'99), LNCS 1628, 43-66. Springer-Verlag, 1999. [6]
V. Bono and M. Bugliesi. Interpretations of Extensible Objects and Types. In Proceedings 12th International Symposium on Fundamentals of Computing Theory (FCT'99), LNCS 1684, 112-123. Springer-Verlag, 1999. [7]
Proceedings of conferences.
V. Bono, A.J. Patel, V. Shmatikov, J.C. Mitchell. A Core Calculus of Classes and Objects. In Mathematical Foundations of Programming Semantics, volume 20 of Electronic Notes in Theoretical Computer Science, 1-22, Elsevier, 1999. [8]
