Forskningen min er for tiden rettet mot avhengig typeteori.

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. Homotopi-typeteori (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 en model for multimengder og en forenkling av modellen for mengelære i homotopi-typeteori. Videre, har jeg bidratt til teorien for beholdere, en modell for datastrukturer i typeteori – ved å utvide begrepet til data strukturer med symmetrier.

Vitenskapelig artikkel

• Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad (2024). On planarity of graphs in homotopy type theory. (ekstern lenke)
• Gratzer, Daniel; Gylterud, Håkon Robbestad; Mörtberg, Anders et al. (2024). The category of iterative sets in homotopy type theory and univalent foundations. (ekstern lenke)
• Forssell, Jon Henrik; Gylterud, Håkon Robbestad; Spivak, David I (2020). Type theoretical databases. (ekstern lenke)
• Gylterud, Håkon Robbestad (2019). Multisets in type theory. (ekstern lenke)
• Gylterud, Håkon Robbestad (2018). From multisets to sets in Homotopy Type Theory. (ekstern lenke)

Vitenskapelig foredrag

• Gylterud, Håkon Robbestad (2020). Non-wellfounded sets in HoTT. (ekstern lenke)
• Prieto Cubides, Jonathan Steven; Gylterud, Håkon Robbestad (2019). Planar graphs in HoTT. (ekstern lenke)
• Gylterud, Håkon Robbestad (2019). Quote operations in dependent type theory. (ekstern lenke)
• Gylterud, Håkon Robbestad (2017). Quote operations in λ-calculus and type theory. (ekstern lenke)

Se en full oversikt over publikasjoner i Cristin