Postdoktor i Theory and Implementation of Agda

Göteborgs universitet / Datajobb / Göteborg
Observera att sista ansökningsdag har passerat.

Visa alla datajobb i Göteborg, Mölndal, Partille, Kungälv, Lerum eller i hela Sverige
Visa alla jobb hos Göteborgs universitet i Göteborg, Partille, Lysekil, Uddevalla, Vänersborg eller i hela Sverige

Göteborgs universitet möter samhällets utmaningar med mångsidig kunskap. 37 000 studenter och 6 000 medarbetare gör universitetet till en stor och inspirerande arbetsplats, flödande av kunskap och idéer. Stark forskning och attraktiva utbildningar lockar forskare och studenter från hela världen. Göteborgs universitet är miljöcertifierat och arbetar aktivt för hållbar utveckling. Med ny kunskap och nya perspektiv bidrar universitetet till en bättre framtid.

Universitetet arbetar aktivt för en arbetsmiljö med jämställda förhållanden och sätter värde på de kvalitéer mångfald tillför verksamheten.

Institutionen för data- och informationsteknik har en internationell prägel med cirka 240 anställda från över 30 olika länder. Institutionen är en integrerad institutionen med både Göteborgs universitet och Chalmers tekniska högskola som huvudmän. Anställningen är placerad vid avdelningen för datavetenskap vid institutionen, med Göteborgs universitet som arbetsgivare.

Ämne
Theory and Implementation of Agda

Ämnesbeskrivning
Research theoretical foundations and provide efficient implementations of dependently typed pattern matching in conjunction with subtyping, user-defined rewrite rules, and modal extensions of type theory.

Publiceringsdatum
2017-07-11

Dina arbetsuppgifter
Tjänsten kommer att bestå av forskning om typteori och sin implementation, motsvarande cirka 50 % av heltid. Utöver detta kommer arbetsuppgifter inom utveckling, dokumentering, och underhåll av Agda ingå med cirka 50 %.

Arbetet består av att utveckla effektiva lösningar för implementering av typteori på ett matematiskt rigoröst sätt och välstrukturerad Haskell-kod för dessa lösningar som del av den befintliga typteori implementering Agda. Och dokumentera de erhållna teoretiska lösningarna och deras realiseringar. Möjliga ämnen är beroende pattern matchning, subtyping, sized types, användardefinierade omskrivningsregler och modala förfiningar av typteori (linearitet, bevis-irrelevans, metaprogrammering).

Behörighet
Behörighet för anställning som lärare finns angivna i 4 kap 3 - 4 § Högskoleförordningen samt Göteborgs universitets egna anställningsordning.

Behörighet att anställas som postdoktor är den som vid sista ansökningsdag innehar en doktorsexamen i relevant ämnesområde, till exempel inom datavetenskap eller software engineering. Eftersom anställning som postdoktor utgör en meriteringsanställnng för juniora forskare riktar vi oss främst till den som har en doktorsexamen som inte är äldre än 3 år räknat från sista ansökningsdag. Även den som avlagt examen tidigare kan komma ifråga om särskilda skäl föreligger.

Bedömningsgrund
Bedömningsgrunder vid anställning som lärare finns angivna i 4 kap 3 - 4 § Högskoleförordningen samt Göteborgs universitets egen anställningsordning.

Doktorsexamen i relevant forskningsområde. Flera publikationer i internationella tidskrifter. Goda kunskaper och erfarenhet av ovan beskrivna metoder. Dokumneterad god förmåga att uttrycka sig i tal och skrift.

Den sökande behöver solid erfarenhet av teori och teknologi av beroende typteori och utmärkt kunskap om programmeringsspråket Haskell. Ideelt har kandidaten arbetat och publicerat i en eller flera av följande aspekter av typteori: dependently-typed pattern matching, subtyping, sized types, user-defined rewrite rules eller modal extensions of type theory (linearity, proof-irrelevance, meta-programming).

Den sökande behöver djupa kunskaper om semantiken för kubisk typteori och kunna bidra både till utvecklingen av implementeringen av teorin i Haskell och till ytterligare teoretisk analys av detta system.

Anställning
Anställningsform: Tidsbegränsad anställning, centralt kollektivavtal för anställning av postdoktorer
Omfattning: 100 %
Placering: Institutionen för data- och informationsteknik, Göteborg
Tillträde: 2017-10-01

Kontaktuppgifter för anställningen
Avdelningschef Peter Dybjer, 031-772 1035 eller e-post: peterd@chalmers.se

Frågor om anställningsförfarandet: HR-specialist Anna Skanse Bråse, 031 - 772 8167 eller på e-post:anna.skanse@chalmers.se

Fackliga organisationer
Fackliga företrädare vid Göteborgs universitet hittar du här: http://www.gu.se/omuniversitetet/aktuellt/lediga-jobb/fackliga-kontaktpersoner

Så ansöker du
Du söker anställningen via Göteborgs universitets rekryteringsportal genom att klicka på knappen "Ansök".

För fullständig annons se http://www.gu.se/omuniversitetet/aktuellt/lediga-jobb

Ansökan ska vara inkommen senast: 2017-07-31

Till bemannings- och rekryteringsföretag och till dig som är försäljare: Göteborgs universitet anlitar upphandlad annonsbyrå i samband med rekrytering av personal. Vi undanber oss vänligen men bestämt direktkontakt med bemannings- och rekryteringsföretag samt försäljare av jobbannonser.

Varaktighet, arbetstid
Heltid/ Ej specificerat

Ersättning
månadslön

Så ansöker du
Sista dag att ansöka är 2017-07-31
Klicka på denna länk för att göra din ansökan

Företag
Göteborgs universitet

Adress
Göteborgs universitet
Chalmers Tekniska Högskola
41296 Göteborg

Kontorsadress
Chalmers Tekniska Högskola

Jobbnummer
3600000

Observera att sista ansökningsdag har passerat.

Postdoktor i Theory and Implementation of Agda

Prenumerera på jobb från Göteborgs universitet