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.
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.
- Mer informasjon om Coq finner du her:
The Coq Proof Assistant
Wikipedia - For mer informasjon om formalisering av programmeringsspråk i Coq, se
https://softwarefoundations.cis.upenn.edu/