Fra endelighet til robust programvare

Datamaskiner styrer mye i dagens samfunn, og i noen tilfeller vil en "blåskjerm" være en katastrofe. Vi ønsker å være sikker på at programvaren som styrer en pacemaker eller et fly ikke slår seg av i tide og utide. For å bli virkelig sikker kan vi bevise matematisk at programvaren aldri slår seg av ukontrollert: at den kan fortsette i det uendelige.Uheldigvis er det komplisert å bevise ting om programvare, så komplisert at vi trenger hjelp av et annet stykke programvare for å hjelpe oss med å holde styr på beviset. Men da trenger vi et begrep om endelighet og uendelighet som datamaskinen kan jobbe med.Avhandlingen bruker konstruktiv matematikk for å undersøke forskjellige former for endelighet, avgjøre styrkeforhold mellom dem, og bevise nye egenskaper om de forskjellige konseptene.Konstruktiv matematikk er en gren av matematikk hvor beviser korresponderer med algoritmer, og ved å studere konsepter som endelighet konstruktivt får vi resultater som vi kan tilbakeføre til datamaskinen. 

Om kandidaten

: Erik Parmann (1986) er født i Bergen og har en mastergrad fra Universitetet i Bergen (2011).