NY DOKTORGRAD
Effektiv utvikling av korrekte datasystemer
 |
"The Institution of Multialgebras - a general framework for algebraic software development"
Formelle (matematiske) metoder har vist seg lovende for å kunne utvikle korrekte og effektive datasystemer. Avhandlingen viser hvordan multialgebraer kan anvendes som et generelt utviklingsverktøy for programutvikling. En algebra er en matematisk struktur hvor operasjoner returnerer elementer. Multialgebraer generaliserer algebraer ved at en tillater at operasjoner returnerer mengder av elementer.
I starten av avhandlingen presenteres et spesifikasjonsspråk for multialgebraer. En viser også hvordan multialgebraer er relatert til andre algebraiske rammeverk, samt at en gir det matematiske fundamentet som avhandlingen bygger på.
Resten av avhandlingen består av 3 deler.
Slutningssystem for multialgebraer, logiske slutningssystemer brukes for å bevise korrekthet både av spesifikasjoner og av ferdig implementerte datasystemer. Avhandlingen presenterer to nye korrekte og fullstendige logiske slutningssystemer for multialgebraer, som forbedrer tidligere presenterte slutningssystemer for multialgebraer.
Håndtering av feilsituasjoner, dette er et sentralt forskningstema innenfor informatikk. Avhandlingen viser hvordan en kan bruke multialgebraer til å modellere feilsituasjoner. Hvis en operasjon forårsaker en feilsituasjon returneres i utgangspunktet mengden av alle tenkelige verdier for operasjonen. En innskrenker så stegvis verdiene som kan returneres av operasjonen. Prosessen avsluttes ved at en innfører konkrete feilverdier eller at en spesifiserer hvordan en kan utføre unntakshåndtering.
Parameteriserte datatyper, omhandler hvordan en kan bygge opp komplekse datasystemer fra enkle programmoduler. Avhandlingen presenterer en generalisering av eksisterende krav for spesifikasjon av parameteriserte datatyper og viser forskjellige måter for hvordan disse kan settes sammen. Det innføres også et begrep, forfining av parameteriserte datatyper, som tilsvarer at en utvider datasystemer med ekstra funksjonalitet.
Emne for prøveforelesning :
"Categorical semantics of Logic Programming"
Personalia:
Yngve Lamo (32) er født i Brønnøysund og oppvokst i Mosjøen i Nordland. Han tok cand.scient. graden i matematikk ved NTNU i 1996, og jobbet som høyskolelektor ved Høgskolen i Vestfold før han i 1997 ble ansatt i stipendiat-stilling ved Universitetet i Bergen. I 2000 ble han ansatt som høgskolelektor ved Høgskolen i Bergen, siden høsten 2002 har han også vært tilknyttet prosjektet MOSIS ved Institutt for Informatikk UiB.
Tidspunkt og sted for prøveforelesningen:
31.01.2003, kl.
11:30, Rom 2144, Høyteknoligisenteret i Bergen, Thormøhlensgate 55
Tidspunkt og sted for disputasen:
31.01.2003, kl. 14:00, Rom 2144, Høyteknoligisenteret i Bergen, Thormøhlensgate 55
Kontaktpersoner:
Yngve Lamo, tlf. 55 58 75 67 , epost: yla@hib.no
Formidlingsavdelingen v/ mediekontakt Margareth Barndon, tlf. 55 58 90 34 (a), e-post: margareth.barndon@info.uib.no
Avhandlingen kan lånes på Det matematisk-naturvitenskapelige fakultetsbibliotek. For kjøp/bestilling: kontakt kandidaten direkte.