ERC FUNDED PROJECTS

The Aryl hydrocarbon receptor is an evolutionary conserved widely expressed transcription factor that mediates the toxicity of a substantial variety of exogenous toxins, but is also stimulated by endogenous physiological ligands. While it is known that this receptor mediates the toxicity of dioxin, this is unlikely to be its physiological function. We have recently identified selective expression of AhR in the Th17 subset of effector CD4 T cells. Ligation of AhR by a candidate endogenous ligand (FICZ) which is a UV metabolite of tryptophan causes expansion of Th17 cells and the induction of IL-22 production. As a consequence, AhR ligation will exacerbate autoimmune diseases such as experimental autoimmune encephalomyelitis. Little is known so far about the impact of AhR ligands on IL-17/IL-22 mediated immune defense functions. IL-22 is considered a pro-inflammatory Th17 cytokine, which is involved in the etiology of psoriasis, but it has also been shown to be a survival factor for epithelial cells. AhR is polymorphic and defined as high or low affinity receptor for dioxin leading to the classification of high and low responder mouse strains based on defined mutations. In humans similar polymorphisms exist and although on the whole human AhR is thought to be of low affinity in humans, there are identified mutations that confer high responder status. No correlations have been made with Th17 mediated immune responses in mice and humans. This study aims to investigate the role of AhR ligands and polymorphisms in autoimmunity as well as protective immune responses using both mouse models and human samples from normal controls as well as psoriasis patients.

1 242 352 €

Start date: 2009-02-01, End date: 2014-01-31

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

One of the fundamental goals of theoretical computer science is to understand the possibilities and limits of efficient computation. This quest has two dimensions. The theory of algorithms focuses on finding efficient solutions to problems, while computational complexity theory aims to understand when and why problems are hard to solve. These two areas have different philosophies and use different sets of techniques. However, in recent years there have been indications of deep and mysterious connections between them. In this project, we propose to explore and develop the connections between algorithmic analysis and complexity lower bounds in a systematic way. On the one hand, we plan to use complexity lower bound techniques as inspiration to design new and improved algorithms for Satisfiability and other NP-complete problems, as well as to analyze existing algorithms better. On the other hand, we plan to strengthen implications yielding circuit lower bounds from non-trivial algorithms for Satisfiability, and to derive new circuit lower bounds using these stronger implications. This project has potential for massive impact in both the areas of algorithms and computational complexity. Improved algorithms for Satisfiability could lead to improved SAT solvers, and the new analytical tools would lead to a better understanding of existing heuristics. Complexity lower bound questions are fundamental but notoriously difficult, and new lower bounds would open the way to unconditionally secure cryptographic protocols and derandomization of probabilistic algorithms. More broadly, this project aims to initiate greater dialogue between the two areas, with an exchange of ideas and techniques which leads to accelerated progress in both, as well as a deeper understanding of the nature of efficient computation.

1 274 496 €

Start date: 2014-03-01, End date: 2019-02-28

This project aims to improve evidence-based decision-making. What makes it radical is that it plans to do this in situations (common for critical risk assessment problems) where there is little or even no data, and hence where traditional statistics cannot be used. To address this problem Bayesian analysis, which enables domain experts to supplement observed data with subjective probabilities, is normally used. As real-world problems typically involve multiple uncertain variables, Bayesian analysis is extended using a technique called Bayesian networks (BNs). But, despite many great benefits, BNs have been under-exploited, especially in areas where they offer the greatest potential for improvements (law, medicine and systems engineering). This is mainly because of widespread resistance to relying on subjective knowledge. To address this problem much current research assumes sufficient data are available to make the expert’s input minimal or even redundant; with such data it may be possible to ‘learn’ the underlying BN model. But this approach offers nothing when there is limited or no data. Even when ‘big’ data are available the resulting models may be superficially objective but fundamentally flawed as they fail to capture the underlying causal structure that only expert knowledge can provide. Our solution is to develop a method to systemize the way expert driven causal BN models can be built and used effectively either in the absence of data or as a means of determining what future data is really required. The method involves a new way of framing problems and extensions to BN theory, notation and tools. Working with relevant domain experts, along with cognitive psychologists, our methods will be developed and tested experimentally on real-world critical decision-problems in medicine, law, forensics, and transport. As the work complements current data-driven approaches, it will lead to improved BN modelling both when there is extensive data as well as none.

1 572 562 €

Start date: 2014-04-01, End date: 2018-03-31