Nyheter

• Nyhetsarkiv

Abstrakt matematik och datavetenskap i växelverkan ger säkrare teknik

Nyhet: 2010-01-07

Färre fel och buggar i våra datorer och säkrare robotteknik. Det kan bli några av resultaten av professor Thierry Coquands banbrytande arbete med att förbättra kvaliteten på datorbaserade beräkningar. Forskningen bedrivs inom det europeiska projektet Formath som nu får 25 miljoner kronor i stöd av EU.

– Vår förhoppning är att Formathprojektet ska kunna vidareutveckla matematikernas möjligheter att använda sig av datorbaserade beräkningar och också kvaliteten på dessa, säger professor Thierry Coquand. Förutom matematiken som sådan, är vår vision att forskningen inom Formath i förlängningen kommer att ha inverkan på alla områden inom mjukvaruutveckling, där mjukvaran möter en fysisk verklighet. Det gäller t.ex. medicinsk bildbehandling som datortomografi, eller olika typer av robotar.

Professor Thierry Coquand, institutionen för data- och informationsteknik, står som projektkoordinator för Formath – ett europeiskt forskningssamarbete som tilldelats nära 25 milj. kronor (2,3 milj €) från EU för tre år framöver. 

Formath står för ”Formalisation for Mathematics” och handlar om att utveckla system för att kontrollera korrektheten i matematiska bevis. Formath ett europeiskt forskningssamarbete som har tilldelats nära 25 milj. kronor från EU för tre år framöver. Projektet bottnar i ett närbesläktat forskningssamarbete, TYPES, som sträcker sig 20 år tillbaka i tiden. De pengar man nu får från EU kommer att användas till att vidareutveckla och användaranpassa programvaran ”Interactive Proof Checker” som säkerställer korrektheten i matematiska bevis.

Projektet Formath innebär också en växelverkan mellan datavetenskap och matematik. Med mjukvaran ”Interactive Proof Checker” skapas nya förutsättningar för matematiken – och de nya möjligheterna inom matematiken kommer sedan i sin tur att användas för utvecklingen mot ännu mer korrekt programvara. Som ger möjlighet att ytterligare finjustera matematiken etc.

– Matematiken spelar redan en mycket central roll för designen av sofistikerade system i vårt dagliga liv, säger Thierry Coquand. Den här användningen av matematiken kommer att öka och frågor som korrekthet och pålitlig specificering av hur systemen ska tolkas kommer att bli allt viktigare.

I Formathprojektet ingår sammanlagt fem forskargrupper från fyra universitet, där professor Thierry Coquand vid Göteborgs universitet står som koordinator för projektet. Övriga universitet som ingår är INRIA i Frankrike, Radboud Universiteit Nijmegen i Nederländerna och Universidad de La Rioja i Spanien. Ett laboratorium gemensamt för INRIA-Microsoft är också involverat, där Georges Gonthier på Microsoft är projektledare för en av delarna.

Pengarna har sökts inom den öppna klass som kallas FET, Future and Emerging Technologies, där det normalt sett är mycket svårt att få igenom sina ansökningar. Därför är man extra glad för det här anslaget.

Thierry Coquand har samtidigt med EU-pengarna för Formath tilldelats ett personligt ERC Advanced Grant på drygt 20 milj. kronor för sin forskning inom grundläggande matematik. ERC-stipendiet har funnits sedan år 2008 och riktar sig till europeiska seniora forskare i världsklass. Projektet Formath kan ses som en tillämpning av forskningen inom området som tilldelats ERC Advanced Grant.
 

Kontaktinformation:
Professor Thierry Coquand
Institutionen för data- och informationsteknik
Tel: 031-772 10 30

AV: