Håkon Robbestad Gylterud's picture

Håkon Robbestad Gylterud

Associate Professor
  • E-mailHakon.Gylterud@uib.no
  • Visitor Address
    HIB - Thormøhlensgt. 55
  • Postal Address
    Postboks 7803
    5020 Bergen

My research is currently focussed on dependent type theory.

Dependent type theory (à la Marin-Löf) seeks to be a foundation for formal reasoning in mathematics and computer science. Its powerful concept of introduction, elimination and computation rules has proven a robust and extensible way of organising formal reasoning. Homotopy type theory (initiated by the late Vladimir Voevodsky) is a recently developed flavour of dependent type theory – where higher dimensional mathematical objects reside as first-class objects.

My contributions to the field includes a model of multisets and a simplification of the model of set theory in homotopy type theory. Further more, I have contributed to the theory of containers, a model of data structures in type theory, by extending the notion to data structures with symmetries.

Academic article
  • 2020. Type theoretical databases. Journal of Logic and Computation.
  • 2019. Multisets in type theory. Mathematical proceedings of the Cambridge Philosophical Society (Print). 1-18.
  • 2018. From multisets to sets in Homotopy Type Theory. Journal of Symbolic Logic (JSL). 1132-1146.
Academic lecture
  • 2020. Non-wellfounded sets in HoTT.
  • 2019. Quote operations in dependent type theory.
  • 2019. Planar graphs in HoTT.
  • 2017. Quote operations in λ-calculus and type theory.

More information in national current research information system (CRIStin)