Probleemstelling: Een gepland onderdeel van het vak 'Theory of programming and types' is het bewijzen van eigenschappen van programmeertalen en typesystemen met behulp van de dependently typed taal Agda. Opgaven zullen waarschijnlijk definities en bewijzen van een aantal simpele taaltjes uit 'Types and Programming Languages' van Benjamin C. Pierce in Agda uitdrukken en vervolgens de student vragen een aantal 'gaten' hierin in te vullen. Het boek begint met het specificeren van een simpele taal die bestaat uit rekenkundige expressies, gevolgd door de ongetypeerde lambda-calculus. Hierna, in hoofdstuk 2, worden types en typeregels aan die eerste taal toegevoegd en worden er bewijzen geleverd over verschillende eigenschappen hiervan. Daarna wordt op vergelijkbare wijze de simpel getypeerde lamdba-calculus beschreven, gevolgd door allerlei extensies die typisch zijn voor functionele talen (bijvoorbeeld producten, sommen, lijsten en recursie). Het tweede hoofdstuk behandeld ook normalisatie (elk programma termineert) van de simpel-getypeerde calculus, variabele verwijzingen (en dus een vorm van staat) en run-time exceptions. Het zou mooi zijn als van verscheidene onderdelen van dit hoofdstuk Agda-opdrachten voor de studenten gemaakt kunnen worden, het liefst op een manier dat er wel interessante aspecten aan bod komen, maar dat het leveren van bewijzen binnen Agda niet te complex wordt. Onderzoeksvraag: Hoe zouden de definities en bewijzen uit 'Theory of programming and types' (en eventueel vergelijkbare bronnen) gerepresenteerd kunnen worden in Agda en welke onderdelen hiervan zouden als opdrachten voor studenten kunnen dienen? Zijn die onderdelen relevant genoeg en wordt het geven van Agda-bewijzen niet de ingewikkeld? Is Agda überhaupt een geschikt platform hiervoor? Onderzoeksmethoden: Om dit te onderzoeken ben ik van plan om te kijken naar de definities en bewijzen die gegeven worden in 'Types and Programming Languages' en andere bronnen over typetheorie. Ook ga ik o.a. kijken naar een vergelijkbaar vak dat gegeven is aan de Chalmers-universiteit en naar 'Software Foundations' door Benjamin C. Pierce et al., waarin uitgelegd wordt hoe de simply-typed lambda calculus, extensies daarvan, en bewijzen over eigenschappen, gerepresenteerd kunnen worden in Coq; ook worden er opgaven gegeven. Vervolgens zal ik zelf proberen een aantal simpele talen, zoals de simply-typed lambda calculus, in Agda uit te drukken en daar bewijzen over te leveren op vergelijkbare wijze als in 'Theory of programming and types'. Ik zal dan een aantal keer een feature aan één van die talen proberen toe te voegen en te kijken hoe de lemma's en definities dan uitgebreid moeten worden. Verwachte uitkomsten: Door dit te doen hoop ik een beoordeling te kunnen maken welke onderdelen wel en welke niet geschikt zouden zijn om voor Agda-opdrachten te gebruiken. Ook wil ik een inschatting maken van de moeilijkheidsgraad van dit soort taken en de problemen die kunnen optreden. Hiermee hoop ik een aantal opdrachten te kunnen produceren die ook daadwerkelijk tijdens het vak 'Theory of programming and types' gebruikt kunnen worden.