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.