Antal poäng: 5. Betygskala: TH. Valfri för: D3, E3, F3. Kursansvarig: Univ.lektor Lennart Andersson, Lennart.Andersson@cs.lth.se, Inst f datavetenskap. Förkunskapskrav: EDA027 Algoritmer och datastrukturer, FMA410 Matematik, endimensionell analys, FMA420/FMA425 Linjär algebra och FMA430/FMA435 Flerdimensionell analys. Prestationsbedömning: Skriftlig tentamen. Studenterna förväntas presentera lösningar till förelagda problem vid seminarier. Detta tillgodoräknas vid första ordinarie tentamenstillfälle. Övrigt: Kursen är periodiserad. Den planeras ges våren 05 och därefter våren 2007. Kursen kan komma att ställas in vid mindre än 20 anmälda deltagare. Hemsida: http://www.cs.lth.se/Education/Courses/EDA145.

Mål
Kursen skall

• ge förmåga att formellt beskriva syntax och semantik för programspråk.

• ge förmåga att bevisa egenskaper hos program.

• ge 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.