ºÚÁϳԹÏ×ÊÔ´

Forskningen min er for tiden rettet mot avhengig typeteori.

(à la Martin-Löf) er utviklet som et fundament for formell resonering for bÃ¥de matematikk og datavitenskap. Typeteoriens konsept om introduksjon, eliminasjon og beregning har vist seg Ã¥ være en robust mÃ¥te Ã¥ organsisere formelle resonnement og har utvidelser til mange bruksomrÃ¥der. (et felt grunnlagt av Vladimir Voevodsky)  er en nylig utviklet variant av avhengig typeteori, hvor høyere-dimmensjonale matematiske objekter er første-klasses innbygere i det formelle systemet.

Blant mine bidrag til feltet finner man . Videre, har jeg bidratt til teorien for beholdere, en modell for datastrukturer i typeteori – ved å utvide begrepet til .