Project 144029

Models, Languages, Types, and Processes in Computing

Leader: Prof. Silvia Ghilezan



Technology for building accurately specified and reliably correct computer systems is of deep interest for industry. This is a long-term problem that  requires progress in many areas. The use of formal logic for specification and reasoning about systems and of strongly typed programming languages with inherent correctness properties, are well accepted and necessary part of the solution. The aim of our research activities is directed towards the application of type theory and proof theory to computing, the construction of models and types in global computing and analysis of digital objects. In the framework of this project we will investigate constructive interpretations of classical logic related to programming languages. Technologies for formal reasoning based on type theory and proof theory will be developed. Techniques for programming languages for global computing as well as models for distributed mobile systems will be investigated.  Methods for coding of digital objects will be further developed.

 The members of this project are participating in two European projects, one of them is  FP6 IST-FET project «TYPES-Types for Proofs and Programs», FP6-510996, (2004-2007) and the other is from CEEPUS II programme "Medical imaging & Medical information processing", CII-AT-0042-01-0506, (2005-2007). In this way the research within this project will be supported by these two European projects and directly connected to ongoing international research in this area.


Subject of the Research

The Project addresses the following topics:

Type theory is the foundation of programming languages with types, such as Java, OCAML, Haskell, ML. Type theory is, at the same time, an allternative to set theory in the foundations of mathematics. It is based on the stratification of types in order to avoid uncoherence.  Research in constructive mathematical logic, which is a base of type theory, is a mainstream because of its application to computer science. In the framework of this project, we propose research on constructive interpretations of classical logic related to the programming language SCHEME, which call for more attention. We will focus on control operators, separation, and characterization of strong normalization in those calculi which correspond to program termination in the underlying programming language, as well as on models based on type theory. Concepts of subtyping, isomorphism between types, and retraction of types will be a subject to our investigation. These concepts are of great importance in the foundations of computer science because they provide effective solutions for security and safety. The proof assistant COQ is based on the calculus of constructions which incorporates types depending on other types and terms. Our investigation will be in the formalization of mathematics within COQ. This research is supported by the European FP6 IST-FET project «TYPES-Types for Proofs and Programs», FP6-510996, (2004-2007).

“Global computing systems” denotes infrastructures of global computer networks (internet, world-wide-web). Global computing systems became more and more complex due to their ubiquitousness and inevitableness in the contemporary world.  A new conceptual dimension of computing, where widespread entities exchange data, migrate from one location to another, and communicate among themselves, has gained an important role and demands a theoretical foundation based on mathematical modelling. Global computing deals with modelling and designing of global computing systems. The research is directed towards systems with the following characteristics:
The systems which are composed of autonomous computational entities where activity is not centrally controlled, either because global control is impossible or impractical, or because the entities are created or controlled by different owners.
      - The computational entities which are mobile, due to the movement within a physical platform or by movement of the entity from one platform to another.
     - The configurations which vary over time since the systems are open to the introduction of new computational entities and likewise their deletion. The behaviour of the entities may vary over time.
      - The systems which operate with incomplete information about the environment, since information becomes rapidly out of date and mobility requires information about the environment to be discovered.

 Digital image analysis is a modern field within mathematics and computer science. It has wide applicability to many other fields, especially to medicine, where new imaging technologies (CT, MRA, PET) require new methods for the analysis of images. Approaches based on modelling of digital images as fuzzy sets have provided powerful tools, supported by a fast development of computer technology. Avoiding classical binarization approaches, by allowing partial membership of an element to a (fuzzy) set, valuable information is preserved in the image and used during the analysis process, which highly improves accuracy and precision of the results. Application of fuzzy sets in shape analysis requires research related to mathematical modelling of discrete fuzzy shapes and their relevant properties. While the theory of continuous fuzzy sets is  well-developed, the discrete case, present in digital images,  is far less studied. It is also needed to develop algorithms for efficient handling of the larger amounts of data, present in fuzzy representations. This research is supported by the European CEEPUS II program project "Medical imaging & Medical information processing", CII-AT-0042-01-0506, (2005-2007).


Importance of the Planed Research

The addressed topics are related to three different research fields, which are all of high importance in contemporary information society. That raises the importance of the  research proposed by the Project. Type theory is inbuilt in the foundations of computer science, global coputing is an inevitable and more and more present concept in our modern  world, while digital image analysis has become one of the important applications of computer science in everyday life. Active on-going international reserach within all these fields illustrates the actuality of the proposed Project. Gathering these topics within one Project is motivated by the intention to provide the environment for their mutual interaction and mutual stimulation. An important common point for all the addressed research topics is their strong mathematical foundation and background. The planned reserch will take a direction of both developing  mathematical models, and of using the developed models in different applications. The interaction between the theoretical results and the demands of the practice will be both a driving force, and an important positive result of the proposed research.

An important issue is the continuation and further development of the international collaboration (joint research activities) with leading experts from the University of Turin, ENS Lyon, Uppsala University, and other academic institutions with which the reasearch team has already established successful scientific cooperation.


Research Goal and Planed Project Results

Research goals for each of the addressed topics are:

1. Application of type theory in computing:

2. Global computing:

3. Digital image analysis:


Expected results are a significant number of  publications in international journals,  as well as a number of other publications. An additional   important project goal is continuation of the current international collaboration and its further expansion.