My research is currently focussed on dependent type theory.

Dependent type theory (à la Martin-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

• Prieto-Cubides, Jonathan; Gylterud, Håkon Robbestad (2024). On planarity of graphs in homotopy type theory. (external link)
• Forssell, Jon Henrik; Gylterud, Håkon Robbestad; Spivak, David I (2020). Type theoretical databases. (external link)
• Gylterud, Håkon Robbestad (2019). Multisets in type theory. (external link)
• Gylterud, Håkon Robbestad (2018). From multisets to sets in Homotopy Type Theory. (external link)

Academic lecture

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

See a complete overview of publications in Cristin.