Disputas: Ivar Rummelhoff

Prøveforelesning

Bedømmelseskomité

Reader Dr. Alex Simpson, LFCS, School of Informatics, University of Edinburgh
Professor Dr. Thierry Coquand, Department of Computer Science and Engineering, Chalmers University of Technology
Professor Dr. philos. Herman Ruge Jervell, Institutt for Informatikk, Universitetet i Oslo

Leder av disputas:  Hans Brodersen

Veileder:  Dag Normann

Sammendrag

Typeteori er en gren av formell logikk, men med viktige anvendelser innenfor informatikk. For eksempel brukes typeteori for å sikre at dataprogrammer oppfører seg korrekt. I dette doktorgradsarbeidet har fokus vært på abstrakt typeteori, men deler av avhandlingen har også sammenheng med hvordan matematisk kunnskap kan representeres digitalt og - til syvende og sist - hva matematikk egentlig er.

En type er en samling elementer, for eksemple de naturlige tallene; og en mengde er en del av en type. Hvilke regler som gjelder for mengder kan imidlertid variere. I toposteori er det for eksempel slik at elementene med en gitt egenskap alltid danner en mengde ("mengden av partall" osv.), mens dette ville føre til paradokser i tradisjonell mengdelære. Del 2 i avhandlingen beskriver et et nytt rammeverk for å håndtere denne situasjonen. Det gjør oss også i stand til å formulere presist av hva det vil så å simulere mengder ved hjelp av andre strukturer som f.eks. lister.

Avhandlingens første del dreier seg om såkalte polymorfe typer, som har vist seg svært nyttige innen databehandling. Her består innholdet av diverse resultater om en klasse forholdsvis enkle typer i typeteorien System F som vi kaller Π₁-typer: For det første kan vi avgjøre hvorvidt slike typer er bebodde eller tomme; de tomme typene danner et hierarki; og selv om alle typene har "pene" tolkninger i den enkleste modellen for system F, så finnes det modeller av samme slag hvor dette ikke er tilfelle.

Arbeidet ble utført ved Universitetet i Oslo (Matematisk institutt), Carnegie Mellon University i USA og Institut Mittag-Leffler i Sverige.

Kontaktperson

For mer informasjon, kontakt Yngvar Reichelt.