| In het kader van dit project wordt onderzoek gedaan naar bepaalde zogenaamde constructieve logische systemen, met name de typentheorie van de Zweedse logicus en wiskundige Martin-Loef. Een belangrijk kenmerk van deze logische systemen is dat een wiskundig bewijs dat binnen zo n systeem is geformaliseerd ook meteen een expliciet algoritme levert voor de constructie van de in zo n bewijs voorkomende objecten. De logische eigenschappen van Martin-Loef typentheorie verschillen nogal van die van de -klassieke- logica waarmee een wiskundige gewoonlijk werkt. Om deze speciale eigenschappen, en de verbanden met andere logische systemen, beter te begrijpen maken wij -modellen- van universa van wiskundige objecten die zich gedragen volgens de beschrijving van de typentheorie. Hiertoe worden technieken gebruikt uit de theorie van categorieën, uit de theorie van schoven en uit de recursietheorie. Het project besteedt speciaal aandacht aan het construeren van inductieve en co-inductieve typen |
