Antal poäng: 5. Betygskala: TH. Valfri för: D4, E4, F4, Pi2. Kursansvarig: Universitetslektor Lennart Andersson, Lennart.Andersson@cs.lth.se, Inst f datavetenskap. 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. Hemsida: 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

• Syntax. Definition av språk med reguljära uttryck och grammatiker. Abstrakt representation av program.

• Semantik. Operationell, axiomatisk och denotations-semantik. Bevis av egenskaper hos program, t ex korrekthet och ekvivalens.

• Lambdakalkyl och kombinatorisk logik.

• Domänteori. Semantik för rekursiva definitioner.

• Exekveringsmodeller för programspråk. Unifiering och typhärledning.

Litteratur
Nielson H R, Nielson F: Semantics with Applications: A Formal Introduction. Wiley 1992, ISBN 0471929808