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.
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).
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 goals for each of the addressed topics are:
1. Application of type theory in computing:
further development of constructive interpretations of classical logic;
introduction
of types in control operators and
in separation,
and characterization of strong normalization in programming
languages;
geometrization of proofs and applications.
2. Global computing:
further development of models for distributed mobile systems;
investigations of the progamming language techniques for global computing;
construction of types and logics for safety and accesibility of global computing systems.
3. Digital image analysis:
further development of discrete shape descriptors;
development of mathematical methods appropriate for analysis of dicrete fuzzy sets;
development of algorithms that enable applications of theoretical results;
development of efficient coding schemes for digital objects;
development of algebraic approaches to problems of encoding and enumerating in the area of neural networks.
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.