Menu
MapConnectionsTopicsBulgariaThe Night (K-TRIO)Marie Skłodowska-CurieFor studentsFor teachersMethodologySurprise me
H2020Staff exchange2017–2023

CID · Computing with Infinite Data

Horizon 2020 — Marie Skłodowska-Curie Actions

Duration
2017-04-01 → 2023-03-31
EU contribution
€958,500
Participants
21
Scheme
MSCA-RISE

Lines connect the coordinator with its partners. CORDIS does not always give exact coordinates for projects before 2014. These points are placed at city or country level.

Results in brief

Computing with Infinite Data

The joint research in this programme studies important aspects---both theoretical as well as applied---of computing with infinite objects such as decimal fractions, to mention a key example. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications. More and more applications require the use of computers, but in many situations, computer programs can present inaccuracies due to, for example, rounding errors. However, software inaccuracies can create vulnerabilities which can have unexpected consequences. For example, the first Ariadne 5 launch (a rocket used by the European Space Agency) failed due to that kind of inaccuracies. We develop tools which can help resolve these inaccuracies. The problem is that there is a dissociation between the mathematical theory and its implementation in computer programs. One way out of the problem is to formally prove the correct functioning of engineering applications: The autopilot in an aircraft must work flawlessly, e.g.. Human life depends on the technology being correct at all times. Software is usually tested against a variety of possible scenarios. However, this does not guarantee that the software is completely safe. Vulnerabilities can still exist and can have unintended consequences. Using infinite-precision data helps to develop tools to formally prove that programs function according to their respective requirements, which means that we can be sure that the software works correctly. In another part of the investigation, we would like to understand which problems are inherently difficult or even impossible to solve with the help of computers, and how do they fundamentally differ from easier problems. This knowledge is valuable for software developers, since they do no longer need to spend their time for searching for alternatives in such cases. Work on all of these objectives has been very successful: The logical system for specifying algorithms and extracting algorithms from proofs has been dramatically extended and improved: constructive reasoning is seamlessly integrated with classical logic; an extension for specifications of concurrent processes at a very high level is available and has proven practically useful since it improves efficiency; computational garbage can be completely avoided; computational complexity of computation on infinite data can be controlled through precise estimates of look-ahead. For several important types of differential equations appearing in physics and engineering, the intrinsic complexity of solving them has been determined. On the applied side, existing software packages using infinite-precision data have been further extended and the interplay of the different packages has been facilitated.

Data: CORDIS, © European Union

Project objective

The joint research in this programme will study important aspects—both theoretical as well as applied—of computing with infinite objects. A central aim is laying the grounds for the generation of efficient and verified software in engineering applications. A prime example for infinite data is provided by the real numbers, most commonly conceived as infinite sequences of digits. While most applications in science and engineering substitute the reals with floating point numbers of fixed finite precision and thus have to deal with truncation and rounding errors, the approach in this project is different: exact real numbers are taken as first-class citizens and while any computation can only exploit a finite portion of its input in finite time, increased precision is always available by continuing the computation process.This project aims to bring together the expertise of specialists in mathematics, logic, and computer science to push the frontiers of our theoretical and practical understanding of computing with infinite objects. Three overarching motivations drive the proposed collaboration:Representability. Cardinality considerations tell us that it is not possible to represent arbitrary mathematical objects in a way that is accessible to computation. We will enlist expertise in topology, logic, and set theory, to address the question of which objects are representable and how they can be represented most efficiently.Constructivity. Working in a constructive mathematical universe can greatly enhance our understanding of the link between computation and mathematical structure. Not only informs us which are the objects of relevance, it also allows us to devise always correct algorithms from proofs.Efficient implementation. We also aim to make progress on concrete implementations. Theoretical insights from elsewhere will be tested in actual computer systems; obstacles encountered in the latter will inform the direction of mathematical investigation.

Original text from CORDIS.

Participants

  • UNIVERSITAET SIEGEN · SiegenCoordinatorGermany
  • ASTON UNIVERSITY · BirminghamUnited Kingdom
  • Fachhochschule Dortmund · DortmundGermany
  • INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET AUTOMATIQUE · Le Chesnay CedexFrance
  • INSTITUTION OF THE RUSSIAN ACADEMY OF SCIENCES A.P. ERSHOV INSTITUTE OF INFORMATICS SYSTEMS SIBERIAN BRANCH OF RAS · NOVOSIBIRSKCity levelRussia
  • KOREA ADVANCED INSTITUTE OF SCIENCE AND TECHNOLOGY · DAEJEONSouth Korea
  • LUDWIG-MAXIMILIANS-UNIVERSITAET MUENCHEN · PlaneggGermany
  • NANYANG TECHNOLOGICAL UNIVERSITY · SingaporeSingapore
  • NATIONAL UNIVERSITY CORPORATION JAPAN ADVANCED INSTITUTE OF SCIENCE AND TECHNOLOGY · Nomi IshikawaJapan
  • STOCKHOLMS UNIVERSITET · StockholmSweden
  • SWANSEA UNIVERSITY · SwanseaUnited Kingdom
  • THE UNIVERSITY OF BIRMINGHAM · BirminghamUnited Kingdom
  • UNIVERSIDAD ANDRES BELLO · SantiagoChile
  • UNIVERSIDADE DO ALGARVE · FaroPortugal
  • UNIVERSITA DEGLI STUDI DI PADOVA · PadovaItaly
  • UNIVERSITAT TRIER · TrierGermany
  • UNIVERSITEIT MAASTRICHT · MaastrichtNetherlands
  • UNIVERSITY OF CANTERBURY · ChristchurchNew Zealand
  • UNIVERSITY OF SOUTH AFRICA · PRETORIASouth Africa
  • UNIVERZA V LJUBLJANI · LjubljanaSlovenia
  • University of Cincinnati · CincinnatiUnited States

Links

Data: CORDIS, © European Union