Hjem
Håkon Robbestad Gylteruds bilde

Håkon Robbestad Gylterud

Førsteamanuensis
  • E-postHakon.Gylterud@uib.no
  • Besøksadresse
    Thormøhlensgate 55
    5020 Bergen
    Rom 
    404p1
  • Postadresse
    Postboks 7803
    5020 Bergen

Forskningen min er for tiden rettet mot avhengig typeteori.

Avhengig typeteori (à la Marin-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
  • Vis forfatter(e) 2020. Type theoretical databases. Journal of Logic and Computation. 217-238.
  • Vis forfatter(e) 2019. Multisets in type theory. Mathematical proceedings of the Cambridge Philosophical Society (Print). 1-18.
  • Vis forfatter(e) 2018. From multisets to sets in Homotopy Type Theory. Journal of Symbolic Logic (JSL). 1132-1146.
Vitenskapelig foredrag
  • Vis forfatter(e) 2020. Non-wellfounded sets in HoTT.
  • Vis forfatter(e) 2019. Quote operations in dependent type theory.
  • Vis forfatter(e) 2019. Planar graphs in HoTT.
  • Vis forfatter(e) 2017. Quote operations in λ-calculus and type theory.

Se fullstendig oversikt over publikasjoner i CRIStin.