Antal högskolepoäng: 7,5. Betygsskala: TH. Nivå: A (Avancerad nivå). Huvudområde: Teknik. Undervisningsspråk: Kursen kan komma att ges på engelska. Valfri för: D4, D4pv, E4, E4pv, F4, F4pv, Pi4, Pi4pv. Kursansvarig: Univ.lektor Lennart Andersson, Lennart.Andersson@cs.lth.se, Inst f datavetenskap. Förkunskapskrav: EDA027 Algoritmer och datastrukturer eller EDAA01 Programmeringsteknik - fördjupningskurs, 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. Hemsida: http://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 denotationssemantik. 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. Springer 2007. ISBN 978-1-84628-691-9
Andersson, L: Lecture notes. Datavetenskap.