Theorie, implementatie en toepassing van directed dependent type theories

Dependent type theory is een krachtige logica die toelaat veilige software te ontwikkelen en computergeassisteerd eigenschappen van die software te bewijzen. Dependently-typed talen zoals Agda, Coq en Idris kunnen dan ook zowel gebruikt worden als programmeertaal, als als proof assistant.

De bedoeling van dit doctoraat is om de fundamenten op te stellen van directed dependent type theories (DDTT) door ze te formuleren, te implementeren, en hun consistentie en toepasbaarheid aan te tonen. Onder een DDTT verstaan we een dependent type theory die niet alleen een ingebouwde notie van gelijkheid, maar ook van structuurbewarende transformaties bevat.

Door het concept 'structuur bewaren' op te nemen in de fundamenten van het typesysteem in plaats van het steeds ad hoc te definiëren zoals gebruikelijk is in de klassieke wiskunde, verwachten we allerlei stellingen (inclusief alle parametriciteitsresultaten) en zelfs een aantal operaties gratis te krijgen. Wanneer we bijvoorbeeld een functoriële type-former definiëren (zoals List), verwachten we automatisch een implementatie te krijgen van de functoriële actie ervan (fmap). Dit komt bij uitstek van pas wanneer we willen redeneren over of programmeren met ingewikkeldere concepten, zoals monadetransformaties, die effecten van de ene monade implementeren in termen van de andere, of transformaties tussen wiskundige structuren.

DDTT zal ook leiden tot een beter begrip van subtyping in de context van dependent types. Dit is van bijzonder belang voor de programmeertaal Scala, die subtyping als een essentiële feature bevat en die sinds enige tijd ook in beperkte mate dependent types ondersteunt.