Abstract
In dit project zullen we een beter begrip krijgen van de diepe verbanden tussen bewijzen en algoritmen (computer programma's). Een belangrijke toepassing is het tegelijkertijd ontwikkelen van wiskundige programma's en het bewijs dat ze aan hun specificatie voldoen. Dit laatste is weer onderdeel van een grote doel: het ontwikkelen van een ideale wiskundige assistent. Om deze doelen te bereiken zal ik onderdelen van de wiskunde constructief ontwikkelen, onderzoeken hoe deze wiskunde uit te drukken in de type theory en een computer gebruiken om hier programma's uit te genereren. In dit proces zal ik gebruik maken van de metawiskunde, dat is wiskunde over de wiskunde, en deze ook ontwikkelen. Een van uitdagingen is dat we oneindige objecten, zoals reële getallen, nooit precies in de computer kunnen representeren. Met behulp van een logische methode zijn delen van de wiskunde opnieuw op te bouwen zonder deze oneindige objecten en zonder expressieve kracht te verliezen. Deze methoden moeten nog beter ontwikkeld worden.