Parametriciteit in Type Theorie: Taalprimitieven en Toepassingen

Parametriciteit is een belangrijke eigenschap van functies in de computerwetenschappen, die waardevolle bewijstechnieken aanlevert voor het bestuderen van programmas. Dit is niet alleen het geval voor bewijzen op papier, maar ook bij het opstellen van bewijzen binnen dependently-typed programmeertalen en bewijsassistenten. Bestaande ondersteuning voor (interne) parametriciteit in deze talen laat echter nog te wensen over, zowel op het vlak van expressiviteit (kunnen we standaardgevolgen van parametriciteit bewijzen?) als om technische redenen (vereist grote hoeveelheden meta-theoretische bewijzen). Het doel van dit project is om een volwaardige, intensionele, axiomavrije en intern parametrische typetheorie te ontwerpen, te implementeren en te evalueren. Deze moet voldoende expressief zijn voor het bewijzen van standaardvoorbeelden. Om zo'n typesysteem te construeren, zullen we werken met taalprimitieven die computationele inhoud kunnen geven aan parametriciteit, en met hun denotationele semantiek (specifiek presheafsemantiek), met name het recent voorgestelde transpension type. We zullen het systeem implementeren in een bestaande of nieuwgeconstrueerde bewijsassistent. De kracht en expressiviteit van het bekomen systeem zullen we evalueren op zowel praktisch vlak (door het bestuderen van belangrijke voorbeelden: de inbedding van standaard parametrische calculi en vrije constructies) en op theoretisch vlak (door metatheoretische resultaten te bewijzen over de theorie).