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/