Växelverkan mellan abstrakt matematik och datavetenskap ger säkrare teknik!

Projekt: ForMath

Samverkan mellan Göteborgs universitet, INRIA (Institut national de recherche en informatique et en automatique) 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.

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.

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 under tre år med start 2010.

– Vår målsättning och förhoppning är att ForMathprojektet ska kunna vidareutveckla matematikernas möjligheter att använda sig av datorbaserade beräkningar och också utveckla kvaliteten på dessa, säger 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.

ForMath står för Formalisation for Mathematics och handlar om att utveckla system för att kontrollera korrektheten i matematiska bevis. Projektet bottnar i forskningssamarbetet 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.

Projektet Formath kan ses som en tillämpning av forskningen inom området där Thierry Coquand tilldelats ERC Advanced Grant.

Kontaktinformation:

Professor Thierry Coquand
Institutionen för data- och informationsteknik
Tel: 031-772 1030

ForMaths projektsida