Leerdoelen
Na afloop van deze cursus kunnen de deelnemers:
- Betekenis van imperatieve taalconstructies vastleggen
met inductieve formele technieken. Verschillende beschrijvingsvormen inzetten
en voor een gegeven toepassing een verantwoorde keuze maken. Het effect van
taalontwerpbeslissingen zoals parameteroverdracht en scoperegels verklaren.
- Eigenschappen van programma's specificeren in een formalisme en de correctheid
verifiëren met behulp van geautomatiseerde technieken.
- Berekeningen in functionele talen modelleren in lambda-calculus. Berekeningen
in dit herschrijfmodel analyseren. Typeringssystemen modelleren via typetoewijzingssystemen
in de lambda-calculus.
- Semantiek van logisch programmeren vastleggen via resolutielogica.
- Mogelijkheden en beperkingen van predicaatlogische systemen aangeven met
betekking tot uitdrukkingskracht en beslisbaarheid.
Beginvereisten
Om deze cursus succesvol te kunnen volgen voldoe je aan de volgende voorwaarden.
- Je hebt programmeerervaring met imperatieve, functionele en logische talen
(zoals in de cursussen rond programmeren en kunstmatige intelligentie, eventueel
parallel te volgen).
Je kunt:
- (Programmeer)talen en taaluitbreidingen specificeren met behulp van reguliere
expressies en contextvrije grammatica's (zoals in de cursus Talen en automaten).
- Berekenbaarheid van numerieke operaties aantonen (zoals in de cursus Berekenbaarheid).
- Helder formuleren, zowel bij het motiveren van oplossingen als het weergeven
van wiskundige redeneringen (zoals in de voorafgaande cursussen in de wiskunde
en de theoretische informatica).
- Betekenis van imperatieve taalconstructies vastleggen met behulp van natuurlijke
semantiek (ns) (zoals in de cursus Semantiek en Logica 1)
- Afleidingen voor propositie- en predicaatlogica opstellen in natuurlijke-deductiestijl.
Constructieve en (essentieel) niet-constructieve constructies onderscheiden
(zoals in de cursus Semantiek en Logica 1).
- De relatie tussen syntaxis (taal) en semantiek (model) aanduiden. Bewijs-
en modeltheoretische eigenschappen onderzoeken en hun onderlinge verbanden
verklaren (zoals in de cursus Semantiek en Logica 1).
- Eigenschappen van programma's (waaronder correctheid) aantonen met behulp
van correctheidscalculi.
- Berekeningen in functionele talen modelleren met behulp van termherschrijfsystemen.
Berekeningen in termherschrijfsystemen analyseren, bijvoorbeeld confluentie-
en terminatiegedrag.