**Katedra za matematiku**

**Modeli, jezici, tipovi i procesi u računarstvu**

Projekat Ministarstva nauke i zaštite životne sredine

Trajanje: 2006-2010

Rukovodilac: Prof. dr Silvia Ghilezan

Name | Title | Institution |

Silvia Ghilezan | Professor | Faculty of Engineering, University of Novi Sad |

Jovanka Pantović | Associate Professor | Faculty of Engineering, University of Novi Sad |

Nataša Sladoje | Assistant Professor | Faculty of Engineering, University of Novi Sad |

Jelena Ivetić | Teaching Assistant Trainee | Faculty of Engineering, University of Novi Sad |

Svetlana Jakšić | Research Assistant Trainee | Faculty of Engineering, University of Novi Sad |

Zoran Petrić | Research Professor | Mathematical Institute – Serbian Academy of Sciences and Arts |

Miodrag Kapetanović | Research Assistant Professor | Mathematical Institute – Serbian Academy of Sciences and Arts |

Silvia Likavec | Ph.D | Faculty of Engineering, University of Novi Sad |

Marija Kolundžija | Ph.D. student | Faculty of Engineering, University of Novi Sad |

Dragiša Žunić | Ph.D student | Faculty of Engineering, University of Novi Sad |

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
- global computing
- digital image analysis

**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:

**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.

**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.

**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.

**Matematički modeli u informacionim tehnologijama**

Projekat Pokrajinskog sekretarijata za nauku i tehnološki razvoj AP Vojvodine

Trajanje: 2005-2008

Rukovodilac: Prof. dr. Silvia Ghilezan

Global Computing | ||

National team | Title | Institution |

Silvia Ghilezan | Professor | Faculty of Engineering, University of Novi Sad |

Jovanka Pantović | Associate Professor | Faculty of Engineering, University of Novi Sad |

Jelena Ivetić | Teaching Assistant Trainee | Faculty of Engineering, University of Novi Sad |

Svetlana Jakšić | Research Assistant Trainee | Faculty of Engineering, University of Novi Sad |

Foreign Partner | ||

Mariangiola Dezani-Ciancaglini | Professor | University of Turin, Italy |

Image Processing | ||

Nataša Sladoje | Assistant Professor | Faculty of Engineering, University of Novi Sad |

Tibor Lukity | Teaching Assistant | Faculty of Engineering, University of Novi Sad |

Foreign Partner | ||

Joakim Lindblad | Assistant Professor | Uppsala University, Sweden |

© 2023. Centar za matematiku i statistiku