Projekter vi har finansieret

Vi ønsker at forstå de blå lyn som ofte ses i toppen af tordenskyer, og som kan slå langt op i stratosfæren til 50 km højde. Vi har ikke kendt til dem så længe, og forstod først hvor meget blå aktivitet man kan se i toppen af en tordensky, da den danske astronaut, Andreas Mogensens, videofilmede et tordenvejr fra Den International Rumstation i 2015, Vi har siden, med the Atmosphere-Space Interactions Monitor (ASIM), set et væld af storme med blå aktivitet. ASIM er ledet of DTU Space og blev sendt op i 2018. Med projektet vil vi undersøge, hvordan de blå lyn hænger sammen med den mere almindeligt kendte lynaktivitet, hvilke forhold i atmosfæren, der generer dem og hvordan de påvirker mængden af ozon og andre drivhusgasser i atmosfæren.

Mange, men langt fra de fleste, tal kan udtrykkes som et forhold mellem hele tal. Disse tal kaldes rationale tal. Rationale tal er løsninger til en førstegradsligning med heltalskoefficienter. Selv hvis et tal ikke er løsning til en førstegradsligning med heltalskoefficienter, er det muligt, at det er løsning til en ligning af højere grad. I dette tilfælde kaldes tallet et algebraisk tal. Tal, der ikke er algebraiske, kaldes transcendente tal. Kvadratroden af 2 er et eksempel på et tal, der ikke er rationalt, men som alligevel er algebraisk. Tallet pi er et eksempel på et transcendent tal. Der er mange tal, der optræder i matematikken, hvor vi ikke ved, om tallet er rationalt eller ej, og det er ofte meget svært at afgøre. Endnu sværere bliver det, når vi prøver at afgøre, om et tal er transcendent. I dette projekt studerer vi kriterier, der medfører, at tal med en bestemt type repræsentation ikke kan være rationale eller enddog ikke kan være algebraiske. Vi vil primært se på tal, der kan repræsenteres som en uendelig sum af led, der er givet ved algebraiske (eller rationale) tal. Vi vil også kigge på andre repræsentationer af tal. Det helt store åbne problem i dette forskningsprojekt er et spørgsmål om Riemanns zeta-funktion, der optræder i mange dele af matematikken og specielt i talteorien. Det har været kendt siden 1700-tallet, at funktionsværdierne er transcendente i lige heltal, men de ulige gemmer stadig på store mysterier.

IT-systemer består i dag af adskillige distribuerede enheder, der kommunikerer ved at udveksle beskeder. Den stigende kompleksitet af disse systemer udgør en stor udfordring i forhold til at programmere dem korrekt. Ny forskning har indikeret, at "session types" kan være med til at specificere, hvordan systemer kommunikerer med hinanden og derved mindske fejl i kommunikationen. Formålet med dette projekt er at studere grundlaget for "session types" ved hjælp en såkaldt bevisassistent (på engelsk ”proof assistant”). En bevisassistent er et værktøj, der gør det muligt at bevise egenskaber ved et programmeringssprog. Dette projekt har som mål at formalisere teorien om session types i en bevisassistent, og dermed lægge fundamentet for korrekt integration af maskin-kontrollerede session types i veletablerede mainstream programmeringssprog.

I min forskningsgruppe interesserer vi os for stoffet gamma-hydroxysmørsyre (GHB) - et naturligt forekommende stof i hjernen men også med mange anvendelser. Stoffet er mest kendt som misbrugsstoffet Fantasy, der anvendes som rekreativt stof i nattelivet. Stoffet er endvidere et kendt lægemiddel til behandling af søvnlidelsen narkolepsi. Siden 1980’erne har man vidst, at GHB binder til bestemte områder i hjernen og genkendes særlig kraftigt af et bestemt protein, som dog indtil nu har været ukendt. Vi har for nylig identificeret dette bindingsprotein ved at benytte særligt designede prober, og vist at det er et meget kendt og betydningsfuldt enzym i neuroner, nemlig enzymet calcium/calmodulin-afhængig protein kinase II alpha (CaMKIIa). CaMKIIa er centralt involveret i læring og hukommelse i pattedyr. Således står vi nu overfor at etablere en helt ny sammenhæng mellem GHBs molekylære bindingssted og nervecellers aktivitet. Det ansøgte projekt omhandler molekylære mekanismer af GHB-lignende stoffer på CaMKIIa via den nyligt identificerede bindingslomme. Ved brug af biokemiske, biofysiske og strukturbiologiske metoder vil vi bestemme præcist hvordan GHB-lignende stoffer virker og undersøge, om de kan regulere genfejl i CaMKIIa. Projektet er baseret på et internationalt samarbejde med eksperter indenfor feltet. Vi forventer, at projektet vil afdække nye muligheder indenfor lægemiddeludvikling i hjernens sygdomme.

Transport af tubulin ind i cellens fimrehår: Fimrehår er tynde strukturer på overfladen af vores celler, der fungerer som motorer i bevægelse af cellen eller cellens omgivelser. Derudover findes også ubevægelige fimrehår, de såkaldte primære cilier, der fungerer som sensorer eller antenner, der modtager signaler fra omgivelserne og organiserer mange af cellens signaltransduktionsmekanismer. Vores celler bruger en mekanisme ved navn intraflagellær transport (IFT) til at bygge og vedligeholde cilier. Den vigtigske byggesten i cilier er tubulin molekylet, som kan polymerisere til aflange strukturer, der er nødvendige for cilium formation og stabilitet. Uden korrekt IFT af tubulin kan cellens cilier ikke dannes korrekt hvilket kan resultere i en række sygdomme/syndromer så som blindhed, sterilitet og cyster i nyrerne. I dette forskningsprojekt vil vi afdække, hvordan tubulin molekylet specifikt genkendes og transporteret af IFT systemet. Til dette vil vi benytte os af biokemiske samt struktur- og celle-biologiske metoder. Denne forskning vil føre til en bedre forståelse af hvordan celler konstruerer cilie organeller og hvad der går galt på det molekylære niveau i ciliopati sygdomme hvor cilier ikke dannes korrekt.

Store molekylære komplekser af store proteiner spiller en helt essentiel rolle i mange biologiske processer, som for eksempel i immunforsvaret, som beskytter mod infektioner og fremmede eller unormale celler. Immunforsvaret genkender og angriber bakterier og virus, der trænger ind i kroppen, og det beskytter os dermed mod sygdomme. For at forstå, for eksempel, hvordan immunforsvaret fungerer på molekylært niveau er det nødvendigt at kende strukturen af de komplekser, der er involveret, samt ændringer i strukturen, når komplekserne aktiveres. Dette projekt vedrører en røntgenspredningsteknik (kendt som SAXS), som kan udføres direkte på komplekserne i vand, og som sammen med elektron-mikroskopi, er den væsentligste metode til bestemmelse af strukturen af store biologiske komplekser. Der vil blive udviklet en programpakke til analyse af SAXS-data fra store biomolekylære komplekser baseret på helt nye beregningsmetoder, der vil gøre analysen mere præcis og pålidelig.

Kunstig intelligens (AI) beskæftiger sig med at gøre maskiner i stand til at foretage "intelligente valg". Indenfor AI-planlægning, der er den gren af kunstig intelligens der vedrører intelligente agenter, autonome robotter og ubemandede køretøjer, bygger de "intelligente valg" på at finde en strategi, der ud fra en beskrivelse af verden, de ønskede mål, og de mulige handlinger, opnår de givne mål. At finde disse strategier er et meget komplekst problem, og det bliver derfor ofte løst ved at transformere problemet til et boolean satisfaction (SAT) problem, som kan løses effektivt ved hjælp af moderne såkaldte SAT solvers. Ved første øjekast er det overraskede, at den overstående metode overhovedet er effektiv, da det forventes at være umuligt at løse SAT problemet i polynomiel tid (dette er den berømte P ≠ NP formodning). På trods af dette kan de SAT problemer der fremkommer i AI-planlægning løses særdeles effektivt; selv høj-dimensionale problemer med mere end 1.000.000 variable. Dette formodes at skyldes, at det kun er en meget lille klasse af SAT problemer, der er svære at løse (kræver eksponentiel tid), og at disse problemer ligger på grænsefladen hvor SAT problemet går fra at være underrestringeret til at være overrestringeret. Formålet med dette projekt er at lave et matematisk bevis for gyldigheden af denne berømte formodning, der er kendt som "the satisfiability conjecture".

Hukommelsen er essentiel for vores identitet og evne til at lære. Årtiers forskning har vist at erindringer lagres i et netværk af forbindelser imellem hjerneceller, såkaldte synapser. Hukommelse bygger på styrkelse af forbindelser der bliver brugt, og henfald af forbindelser der ikke bliver brugt. Men hvordan sker dette på molekylært plan? I dette projekt vil vi undersøge en mekanisme der fører til styrkelse af synapser. For at en forbindelse imellem hjerneceller kan blive stærkere, kræver det at synapserne tiltrækker de proteiner der udgør deres molekylære maskineri. Vi vil teste en hypotetisk mekanisme der kan forklare hvordan proteiner bliver tiltrukket til aktive synapser, og forsøge at forstå hvilke proteiner der bliver rekrutteret. Potentielt kan denne hypotese bidrage til at forstå hundredevis af forskellige proteiners funktion. Projektet kan dermed hjælpe os med at forstå hvordan kommunikation imellem nerveceller bliver omsat til de varige ændringer af hjernens forbindelser, der ligger til grund for vores hukommelse.

Kvasarer er nogle af de mest fascinerende objekter vi kender i Universet. De er en slags kosmiske fyrtårne, som lyser så kraftigt, at vi ret nemt kan finde dem og studere lyset fra dem, selv om de er mange milliarder lysår borte. Den kraftige lysudsendelse skyldes, hvilket virker noget paradoksalt, tilstedeværelsen af super-tunge sorte huller med masser på adskillige milliarder gange solens masse. Disse sorte huller skaber populært sagt så dybe huller, at normalt stof kan blive enormt varmt og lysstærk ved at falde ned i dem. Imidlertid er det gradvist blevet klart, at traditionelle metoder til at lokalisere kvasarer på himlen har meget store huller i nettet. Specielt findes der mange kvasarer, hvis optiske farver er blevet røde p.g.a. tilstedeværelsen af store mængder støv-partikler, enten i kvasarens værtsgalakser eller i materiale lyset fra kvasaren passerer undervejs. Sådanne kvasarer er særlig nemme at overse med sædvanlige metoder, da disse metoder beror på, at kvasarer er mere blå end stjerner. I projektet vil vi bruge en ny metode som ikke udvælger kvasarer ud fra deres farver, men i stedet ud fra deres (manglende) bevægelse på himmelkuglen. ESAs Gaia satellit måler i disse år mange milliarder "stjerners" egenbevægelse på himlen. Ved at vælge de "stjerner", der står helt stille kan vi finde kvasarerne blandt stjernerne på en ny og mere komplet måde. I projektet vil vi særligt udnytte denne metode til at bygge et repræsentativt katalog over mere end 15000 kvasarer.

The field of cryptography evolves in a non-linear way, where attacks against conventional techniques launch a new wave of ideas that make the next generation of systems more secure. Every new generation of cryptographic algorithms and implementations is more secure than the previous one that ended up being replaced. Most of public-key cryptography relies on the performance of modular arithmetic involving large numbers to be efficient. However, conventional algorithms to perform these operations are serialized and cannot make full usage of resources available in modern processors. Alternatives for these algorithms are known and estimated to be more efficient in theory, but mysteriously fail to perform well in practice. We want to find out why and optimize these algorithms in a way that they can deliver the expected performance in practice without sacrificing security or correctness. This project deals with the challenges of discovering new algorithms and implementation techniques to accelerate modular arithmetic of cryptographic interest, with a sharp focus on developing formal verification for correctness and implementation security guarantees. We aim to improve performance of state-of-the-art cryptographic algorithms so even small devices can benefit from their security guarantees without spending much resources.