Jonathan Prieto-Cubides's picture

Jonathan Prieto-Cubides

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

    5020 Bergen
  • Postal Address
    Postboks 7803
    5020 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. 

Academic lecture
  • 2019. Planar graphs in HoTT.

More information in national current research information system (CRIStin)

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