Doktorand i typteori

Institutionen för data- och informationsteknik erbjuder grund- och forskarutbildning inom många ämnen: algoritmer, datorarkitektur, datorsäkerhet, distribuerade system, elektronikkonstruktion, formella metoder, logik, nätverk, programvaruteknik, software engineering, språkteknologi och tillförlitliga datorsystem. Det innebär närmare 150 olika kurser på ett 20-tal utbildningsprogram inom både Chalmers och Göteborgs universitet - då institutionen är gemensam mellan dessa. D&IT:s universitetsdel ingår i IT-fakulteten. http://www.chalmers.se/cse

Avdelningen ansvarar för undervisning och forskning inom datavetenskapliga kärnområden som till exempel logik, algoritmer och språk. Forskningen omfattar såväl programmeringsspråk som naturligt språk. Vi är nära kopplade till flera andra vetenskaper, till exempel språkvetenskap, biologi och matematik.

Arbetsuppgifter

Den som antages kommer att bli medlem i Programmeringslogikgruppen vid institutionen och kommer attt delta i dess forskning om typteori, beroende typer och funktionell programmering. Huvuduppgiften är att undersöka Voevodskys univalensaxiom och andra aspekter av univalenta grundvalar för matematik baserad på typteori. Detta kan antingen omfatta formalisering av matematik baserad på dessa grundvalar eller undersökning av dess metateori (t ex om universa och s.k "resizing" axiom).

Valet av forskningsuppgift beror både på doktorandens egna intressen och på gruppens forskninginriktning.

Huvuddelen av doktorandens arbetstid avser egna forskarstudier och egen forskning inkl publicering, deltagande i konferenser mm. Utöver detta ägnas upp till 20% av arbetstiden till institutionsarbete, huvudsakligen undervisning och handledning av studenter. Tjänsten som doktorand är finansierad under fyra år, under förutsättning att tillfredsställande framsteg görs. Detta följs upp vid årliga möten. Eftersom 20% av tjänsten normalt innefattar undervisning och 80% forskning är doktorandperioden normalt fem år.


Behörighet

Den sökande har mastersexamen eller motsvarande (t ex civilingenjörsexamen) i datavetenskap, matematik eller besläktat ämne. Den sökande måste även ha ett genuint intresse för och nyfikenhet på uppgiften, och tidigare erfarenhet i funktionell programmering, typteori, och matematik. Kunskaper om beroende typer är också värdefulla. Den sökande bör också ha utmärkt analysförmåga och kommunikationsförmåga i tal såväl som i skrift.

Grundläggande behörighet till utbildning på forskarnivå har den som har: avlagt examen på avancerad nivå, fullgjort kursfordringar om minst 240 högskolepoäng, varav minst 60 högskolepoäng på avancerad nivå, eller på något annat sätt inom eller utom landet förvärvat i huvudsak motsvarande kunskaper.


Bedömningsgrund

En stark bakgrund i matematik, matematisk logik eller teoretisk datalogi väger tungt vid bedömningen av den sökande. Kunskap om bevisteori, kategoriteori och semantik för programspråk är särskilt värdefull.

Bestämmelser för anställning som doktorand återfinns i förordning SFS 1998:80. Som innehavare får enbart förordnas den som är antagen till utbildning på forskarnivå. Vid tillsättning skall avseende främst fästas vid graden av förmåga att tillgodogöra sig forskarutbildningen. Förutom skyldighet att ägna sig åt egen forskarutbildning kan innehavaren åläggas att fullgöra tjänstgöring som avser utbildning, forskning och administrativt arbete enligt särskilda bestämmelser i förordningen.