Contribution at the European level towards the expected impacts listed in the work programme
The project responds to the increasing expectation for trustworthy, dependable and long-lasting systems by developing reliable compilers not only from the point of view of behaviour but also of performance. Building certified compilers (coming with a machine checked proof of their semantics preservation) is an emerging topic whose relevance is destined to grow in coming years. It looks of high importance for ICT to have methods and tools for producing certifiable systems, and automatic checking of complex invariants (such as preservation of complexity) is a critical step and a major scientific challenge.
| Expected impacts || Contribution of the project
| ICT-relevant, visionary, high quality, long-term research of a foundational nature, involving bright new ideas of high-risk -- high-pay-off, aiming at a breakthrough, a paradigm shift, or at the proof of a novel scientific principle. || The main breakthrough envisaged by the project is the possibility to give a precise performance estimation for the executable (a task that is currently regarded as highly visionary in the compiler community), by creating a (certified) infrastructure allowing to draw conclusions on the target code, while comfortably reasoning on the source. Disposing of a such a tool would allow e.g. to shift programming of critical systems with strong temporal requirements from assembly to a high-level language, with a major beneficial impact on reusability and maintainability. At the same time, it would provide an occasion for rethinking the nature of compilation, measuring the actual impact of the many optimisation phases, and providing a better theoretical status for the many heuristics of current use.
| Research refining the visionary ideas that have gone past the proof-of-concept phase to bring them to the maturity level where they could be taken up by the mainstream ICT programme objectives. || The realization of a tool offering precise and certified performance bounds on the generated code requires an essential paradigm shift of a foundational nature, emphasizing the role of execution paths and their preservation/modification along the the process of compilation. This poses new and interesting semantic challenges, and requires a detailed comparison between different semantic styles to discover the most suitable approach, also in view of its formal encoding and automatic checking. It is also clear that the knowledge gained by such a work could be profitably reused for the treatment high level program transformation techniques, and in general for the study of properties of program.