ERC FUNDED PROJECTS

Mathematical proofs have always been prone to error. Today, proofs can be hundreds of pages long and combine results from many specialisms, making them almost impossible to check. One solution is to deploy modern verification technology. Interactive theorem provers have demonstrated their potential as vehicles for formalising mathematics through achievements such as the verification of the Kepler Conjecture. Proofs done using such tools reach a high standard of correctness. However, existing theorem provers are unsuitable for mathematics. Their formal proofs are unreadable. They struggle to do simple tasks, such as evaluating limits. They lack much basic mathematics, and the material they do have is difficult to locate and apply. ALEXANDRIA will create a proof development environment attractive to working mathematicians, utilising the best technology available across computer science. Its focus will be the management and use of large-scale mathematical knowledge, both theorems and algorithms. The project will employ mathematicians to investigate the formalisation of mathematics in practice. Our already substantial formalised libraries will serve as the starting point. They will be extended and annotated to support sophisticated searches. Techniques will be borrowed from machine learning, information retrieval and natural language processing. Algorithms will be treated similarly: ALEXANDRIA will help users find and invoke the proof methods and algorithms appropriate for the task. ALEXANDRIA will provide (1) comprehensive formal mathematical libraries; (2) search within libraries, and the mining of libraries for proof patterns; (3) automated support for the construction of large formal proofs; (4) sound and practical computer algebra tools. ALEXANDRIA will be based on legible structured proofs. Formal proofs should be not mere code, but a machine-checkable form of communication between mathematicians.

2 430 140 €

Start date: 2017-09-01, End date: 2022-08-31

Cells use an intricate network of intracellular signalling molecules to translate environmental changes, sensed via surface receptors, into cellular responses. Despite their prominent role in regulating every aspect of life, we lack a comprehensive understanding of how signalling networks convey extracellular information into specific bioactivities and fate decisions. To rationally manipulate cell fate, which could fundamentally change the way that we treat human diseases, first we need a systematic understanding of how signalling is initiated and propagated inside the cell. I discovered that specificity of cytokine receptor signalling not only depends on cellular determinants such as receptor density and endocytic trafficking, but can be systematically altered by modulating ligand binding parameters and receptor binding geometries. A fundamentally novel approach combining high-throughput flow cytometry and QMS with engineered cytokine surrogate ligands able to fine-tune signalling responses will generate detailed maps of the signalling networks engaged by cytokines in time and space to unveil the mechanistic basis that allow a receptor to trigger different signal activation programs and bioactivities in response to different ligands. By quantitatively characterizing the signalling programs activated by ligands, using state-of-the-art biochemical, biophysical, structural, genetic and fluorescence imaging techniques, I plan to identify events critical for cellular decisions. By fully characterizing the intracellular signalling network hard-wired inside a cell and understanding its dynamic in response to environmental changes will we be able to comprehend and manipulate the enormous functional plasticity exhibited by cells. TInsights generated will open new fields of investigation where engineered ligands prove indispensable to understand complex biological responses and greatly advance our understanding of cytokine biology and human immunology in health and disease.

1 687 500 €

Start date: 2017-04-01, End date: 2022-03-31

EPIC will automatically construct Evolutionary Program Improvement Collaborators (called Epi-Collaborators) that suggest code changes that improve software according to multiple functional and non-functional objectives. The Epi-Collaborator suggestions will include transplantation of code from a donor system to a host, grafting of entirely new features `grown' (evolved) by the Epi-Collaborator, and identification and optimisation of tuneable `deep' parameters (that were previously unexposed and therefore unexploited). A key feature of the EPIC approach is that all of these suggestions will be underpinned by automatically-constructed quantitative evidence that justifies, explains and documents improvements. EPIC aims to introduce a new way of developing software, as a collaboration between human and machine, exploiting the complementary strengths of each; the human has domain and contextual insights, while the machine has the ability to intelligently search large search spaces. The EPIC approach directly tackles the emergent challenges of multiplicity: optimising for multiple competing and conflicting objectives and platforms with multiple software versions. Keywords: Search Based Software Engineering (SBSE), Evolutionary Computing, Software Testing, Genetic Algorithms, Genetic Programming.

2 159 035 €

Start date: 2017-10-01, End date: 2022-09-30

"The FOGHORN project aims at developing the theoretical and algorithmic foundations of fog-aided wireless networks. This is an emerging class of wireless systems that leverages the synergy and complementarity of cloudification and edge processing, two key technologies in the evolution towards 5G systems and beyond. Fog-aided wireless networks can reap the bene fits of centralization via cloud processing, in terms of capital and operating cost reductions, greening, and enhanced spectral e fficiency, while, at the same time, being able to cater to low-latency applications, such as the ""tactile"" internet, by means of localized intelligence at the network edge. The operation of fog-aided wireless networks poses novel fundamental research problems pertaining to the optimal management of the communication, caching and computing resources at the cloud and at the edge, as well as to the transmission on the fronthaul network connecting cloud and edge. The solution of these problems challenges the theoretical principles and engineering insights which have underpinned the design of existing networks. The initial research activity on the topic, of which the EU is at the forefront, focuses, by and large, on ad hoc solutions and technologies. In contrast, the goal of this project is to develop fundamental theoretical insights and algorithmic principles with the main aim of guiding engineering choices, unlocking new academic opportunities and disclosing new technologies. The theoretical framework is grounded in network information theory, which enables the distillation of design principles, along with signal processing, (non-convex) optimization, queuing and distributed computing to develop and analyse algorithmic solutions."

2 318 719 €

Start date: 2017-06-01, End date: 2022-05-31