• E-mailJonathan.Cubides@uib.no
  • Visitor Address
    Thormøhlensgate 55

    5020 Bergen
  • Postal Address
    Postboks 7803
    5020 Bergen

The context of my research is within the field of formal methods. Precisely, I study mathematical constructions of graph theory in a relatively recent type theory called homotopy type theory.  Many type theories have computational meaning, making them practical to use for computing. One can consider a type theory as a formal system and also as a functional programming language. There is, therefore, no distinction between doing mathematics as proving statements and programming on the computer. For example, I write programs that contain lemmas along with their corresponding proofs. I can assess the correctness of my results with a total level of confidence. The computer checks every statement and each proof. I, of course, must assume the correctness of the proof-checker using this approach.

Academic lecture
  • Show author(s) (2019). Planar graphs in HoTT.

More information in national current research information system (CRIStin)

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