Software styrer meget af infrastrukturen i samfundet. Fejl og sikkerhedsbrister i software kan derfor være ekstremt dyre eller koste menneskeliv. Afhængige typer er en konstruktion i programmeringssprog som programmøren kan bruge til at udtrykke egenskaber ved programmer som kan verificeres som del af programudviklingen. Det vil hjælpe med at konstruere sikre programmer, og at finde fejl tidligt i udviklingen. For eksempel arbejder en gruppe forskere nu på udvikle en sikker udgave af infrastrukturen til sikker internetkommunikation ved hjælp af afhængige typer. Indtil nu har sprog med afhængige typer haft en del begrænsninger, som man har betragtet som nødvendige for den logiske fortolkning af de afhængige typer. For nylig har jeg været med til at udvikle en ny konstruktion som bryder den vigtigste af disse begrænsninger, og tillader generelle rekursive programmer i disse sprog. I dette projekt vil vi vise hvordan denne teknik kan kombineres med algebraiske effekter i programmeringssprog, dvs. handlinger som et program kan udføre mens det kører, f.eks. at læse og skrive til hukommelsen, tage input, træffe ikke-deterministiske valg, etc. Arbejdet i dette projekt er matematisk: De algebraiske effekter kan beskrives som matematiske teorier, og vi studerer hvordan de kan kombineres med en matematisk teori der beskriver vores nye teknik. Målet er at udvikle et udtryksfuldt sprog med afhængige typer hvor man kan skrive programmer og ræsonnere om dem.
