Semantiek en Logica 2 (schakelcursus) 

Ook in deze vervolgcursus leer je formele methoden ontwikkelen en gebruiken in de informatica.

We bekijken geavanceerde formalismen om de operationele semantiek van programmeertalen en taalconstructies vast te leggen. Je zult in deze cursus imperatieve en functionele  talen tegenkomen.

Je leert de formele technieken gebruiken voor taalontwerp, analyse van berekeningen en programmaverificatie (soms met een tool).

Als informaticus zul je formele methoden niet alleen toepassen, maar ook zelf formalismen moeten beoordelen, uitbreiden of ontwikkelen. Daarom gaat deze cursus ook over de eigenschappen van de formele systemen zelf: de metatheorie.

Na afloop van deze cursus kunnen de deelnemers (ovb):

• 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 imperatieve talen: structurele operationele semantiek,parallellisme,nondeterminisme,scope,procedure-evaluatie,recursie
• Specificatieformalismen:JMLtools
• Lambda-calculus:bèta-reductie,confluentie,normalisatie,representatie berekenbare functies,typering,unificatie

• 16 uur groepsgewijs college
• 16 uur hoorcollege
• 2 uur individuele begeleiding
• 18 uur projectwerk
• 32 uur zelfstudie

• oriëntatie (hoorcolleges, 2 uur per week),
  
• zelfstudie (leertaken)
  
• nabespreking (responsiecolleges, 2 uur per week).
  

Een werkstuk (te maken in tweetallen) met een eindbespreking.

De beoordeling is gebaseerd op een aantal deelresultaten. De regeling wordt nog nader bekendgemaakt.

Om deze cursus succesvol te kunnen volgen voldoe je aan de volgende voorwaarden.

• Je hebt programmeerervaring met imperatieve en functionele talen (zoals in de cursussen rond programmeren, 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.

• Hanne Riis Nielson en Flemming Nielson: Semantics with applications, 1999 (via internet: PDF)
• Henk Barendregt en Erik Barendsen: Introduction to lambda calculus (elektronisch via internet)
• Opgavenbundel lambda-calculus
• Aanvullend materiaal

Deze cursus is alleen toegankelijk voor HBO-doorstromers Informatica. Deze cursus volgt op de cursus Semantiek en Logica 1. Bereidt voor op onderwijs waarin formalismen en modellen van berekeningen worden gebruikt. Verdere ontwikkeling van semantiek en typering vindt plaats in de mastercursussen Semantiek en Type Theory.

Dit is de (eerste) helft van het college "Semantiek en Logica 2"

Voor communicatie (mededelingen, e-mail, beoordelingen) gebruiken we Blackboard.