Antal poäng: 5. Betygskala: TH. Valfri för: D4, E4, F4. Kursansvarig: Universitetslektor Lennart Andersson, Lennart.Andersson@cs.lth.se. Förkunskapskrav: EDA025/ EDA026/ EDA027 Algoritmer och datastrukturer. Prestationsbedömning: Skriftlig tentamen och inlämningsuppgifter. Studenterna förväntas presentera lösningar till förelagda problem vid seminarieövningar. Detta tillgodoräknas vid första ordinarie tentamenstillfälle. Webbsida: http://www.cs.lth.se. Övrigt: Kursen kan komma att ställas in vid mindre än 20 anmälda deltagare.

Mål
Kursen skall
- ge förmåga att formellt beskriva syntax och semantik för programspråk.
- förmåga att bevisa egenskaper hos program.
- förståelse för exekveringsmodeller för programspråk.

Innehåll
1. Syntax. Definition av språk med reguljära uttryck och grammatiker. Abstrakt representation av program.
2. Semantik. Operationell, axiomatisk och denotations-semantik. Attributgrammatiker. Bevis av egenskaper hos program, t ex korrekthet och ekvivalens.
3. Lambdakalkyl och kombinatorisk logik.
4. Domänteori. Semantik för rekursiva definitioner.
5. Exekveringsmodeller för programspråk. Unifiering och typhärledning.

Litteratur
Winskel G.: Formal Semantics of Programming Languages. MIT Press, 1993. ISBN 0262731037.