- E-mailJonathan.Cubides@uib.no
- Visitor AddressThormøhlensgate 555020 BergenRoom405M1
- Postal AddressPostboks 78035020 Bergen

My research field is in formal methods. I'm particularly interested in expressing mathematical concepts in (dependent) type theories, specifically, in univalent type theory. Briefly, a type theory is formal system that can serve as a foundation for mathematics where objects are mere constructions of others. What makes really interesting type theory is the huge interaction of ideas coming from fields like category theory, functional programing, homotopy theory, among many others. For a type theorist, there is no distinction between doing mathematics and programming. Type theories have computational meaning that makes them practical to use for computing. Thus, the proofs I produce for my research are verified by the computer in a programming language called Agda. The topic I am currently working with is graph theory and the notion of planarity. This approach gives a theoretical development correct up-to the correctness of the proof-checker.

- 2019. Planar graphs in HoTT.

More information in national current research information system (CRIStin)

At UiB, I started the following open-source projects:

- Mini-HoTT: A library to formalize Univalent Mathematics in Agda.
- Agda-Pkg: A package-manager for the proof-assistant Agda.
- HoTT-cheatsheets: Homotopy type theory cheat sheets to follow INF329.