Jonathan Prieto-Cubides

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.