Research Report Year 2004 - 2005

Area 1: Computer Science

Semantics and Logics of Computation

A - The main research topics have been compositional compilation and dynamic object re-classification for Java-like languages.
Compositional compilation is the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but depends on the compilation context. The papers [6,10] propose an way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables.
The papers [8,9] investigate the interactions between dynamic object re-classification and multithreading by proposing:
    (1) An operational semantics and a type system for a core Java-like concurrent language extended with dynamic object re-classification.
    (2) A translation of the extended language into plain Java, showing how the operational semantics can be implemented with the standard Java multi-threading constructs.

B - Type systems for functional programming languages.
A system of automatic type inference for functional languages, exploiting rank 2 intersection types for typing recursive definitions, has been presented in [14] (a prototype implementation is available at: http://lambda.di.unito.it/pr/).

C – Calculi of parallel and mobile processes have been studied. Our main concern is that of representing and controlling security and resource access properties by means of type systems. This study has been carried out  for calculi which combines ambient and process mobility.  We search for theoretical instruments that support formal reasoning on code migration, on adaptive behaviors, and on context sensitivity. In this ``ubiquitous computing'' scenario mobile computational agents can have different modes of interaction with one another or with the context: consumption or offering of resources, exchange of data and code, possible modification of other components' status. The system presented in [7] addresses security issues of code (process) mobility in a dynamic setting, but still assumes a kind of global knowledge for the resource-access analysis. The one in [12] represent a first step in the direction of considering open ad dynamically reconfigurable systems in which no global assumption is needed.

D - In 2004-2005 Berardi with some co-workers studied a process net maintaining consistency while receiving conflicting data, a commonplace situation when to hierarchically equivalent process produce conflicting answers to the same question. We assume that there is a domain of correct data, equipped some  total ordering on such domain, deciding which datum is closer to the right  answer when two data conflicts. We also assume that data cannot keep on changing forever (no infinite sequence of data getting closer and closer to the right answer exists). Whenever a process receives back a more accurate datum, it replaces it to the current guess, and it discards all computations occurring in the net about the old datum. The theoretical background of this idea has been developed in [3]. The hierarchy of logical principles involved in this kind of reasoning has been subject of a LICS paper [1]. An implementation using continuation has been considered in [3]. On a different but related field two completeness results for proofs and for programming languages has been obtained. A proof of Krivine's intuitionistic proof of classical completion has been developed in [2], and a proof of completeness of a Scott-like semantic of polymorpphic lambda calculus has been obtained in [4] .

Organization of events:  the volumes [5], [13] are the outcome of research events organized by the group.

- Software Products

- Research Grants

Title of the project	Project leader	Funding organization	Kind of grant
TYPES	Main: B. Nordström Local: S. Berardi	EU	Coordination action
McTafi: Metodi costruttivi in Topologia Algebra Fondamenti dell'Informatica.	Main: G. Sambin Local: S. Berardi	MURST	PRIN
Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile	Main: M. Bugliesi Local: M. Coppo	MURST	PRIN
EOS:  Extensible Object Systems	Main: E. Zucca Local: P. Giannini (AL)	MURST	PRIN