Antal högskolepoäng: 7,5. Betygskala: TH. Nivå: A (Avancerad nivå). Undervisningsspråk: Kursen ges på svenska. Valfri för: D3, D3ps, E3ps, F3, Pi4. 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. Kan ställas in: Vid mindre än 20 anmälda. Prestationsbedömning: Skriftlig tentamen. Studenterna förväntas presentera lösningar till förelagda problem vid seminarier. Övrigt: Kursen är periodiserad och ges udda år. Kursen kan komma att ställas in vid mindre än 20 anmälda deltagare. Hemsida: http://www.cs.lth.se/EDA145.

Syfte
Kursen ger ett kvalificerat perspektiv på semantik för programspråk och förmåga att tillgodogöra sig vetenskapliga artiklar inom ett större område av teoretisk datavetenskap än vad kursen täcker.

Mål

Kunskap och förståelse
För godkänd kurs skall studenten

• kunna förstå semantik för programspråkskonstruktioner givna med formell operationell, axiomatisk och denotations–semantik.

• förstå exekveringsmodeller för funktionella språk och logikbaserade språk.

Färdighet och förmåga
För godkänd kurs skall studenten

• kunna ge formell semantik utifrån informella beskrivningar.

• kunna tolka rekursiva definitioner med hjälp av minsta fixpunkter.

• kunna göra beräkningar i lambdakalkyl och kombinatorisk logik.

• kunna konstruera program för typhärledning och unifiering.

• kunna bevisa egenskaper hos program såsom korrekthet och ekvivalens.

Värderingsförmåga och förhållningssätt
För godkänd kurs skall studenten

• kunna tillämpa en kritisk förmåga att värdera programspråkkonstruktioner baserat på deras formella semantiska beskrivningar.

Innehåll
Syntax för programspråk och abstrakt representation av program. Operationell, axiomatisk och denotations–semantik. Bevis av egenskaper hos program. Domänteori och semantik för rekursiva definitioner. Lambdakalkyl och kombinatorisk logik. Exekveringsmodeller för programspråk. Unifiering och typhärledning.

Litteratur
Nielson, H R, Nielson, F: Semantics with Applications: An Appetizer. Boken ersätter en
utgången bok. Förlagsinformation är ännu ej tillgänglig.
Andersson, L: Lecture notes. Datavetenskap 2006.