Logisk resonnering om programmeringsspråk

Denne oppgaven kombinerer verktøy for logikk og formelle bevis med teori for programmeringsspråk som semantikk, type systemer, og statisk analyse. Oppgaven passer for deg som er interessert i både logikk og programmeringsspråk.

Bildet kan inneholde: .

Oppgaven består i å utforske bruk av systemet Coq til å resonnere om programmeringsspråk. Coq er et system for å gjøre formelle bevis. I denne oppgaven vil du bruke dette systemet til å formalisere og resonnere over semantikk for programmeringsspråk. Dette er interessant for utvikling av pålitelige programmer, og dekker mange temaer som blandt annet operasjonell semantikk, type systemer, statisk analyse, Hoare logikk.

Oppgaven passer for deg som både er interessert i logikk og programmeringspråk. Oppgaven kan tilpasses dine interesser i programmering ved at vi sammen bestemmer hva slags programmeringsspråk (eller aspekter ved dette) som skal utforskes.

Emneord: Programmeringsspråk, Teori, Logikk, Analyse
Publisert 22. sep. 2020 14:55 - Sist endret 22. sep. 2020 14:55

Veileder(e)

Omfang (studiepoeng)

60