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.