Welcome to my personal website!

Contact information

About me

My name is Jonathan Prieto-Cubides, and I am a Colombian researcher and explorer from the capital city Bogotá with a passion for mathematics and computer science. I am currently working as a compiler engineer at Heliax designing and implementing the functional programming language Juvix. I am also an ABD PhD Candidate at the University of Bergen in the Department of Informatics. My supervisors there are Håkon R. Gylterud and Marc Bezem. My PhD is around formalising graph-theoretical constructions in Univalent Mathematics. The final document of my PhD thesis will be available soon here. See below some sources regarding this project.

Besides the specific topic of my PhD, I am interested in different areas of mathematics, computer science, and philosophy. By 2023, my current areas of focus include functional programming, the theory and implementation of programming languages, automatic theorem provers, and algorithm design. In the past, I conducted research in the areas of proof reconstruction, natural language processing, and machine learning algorithms.

In addition to my current professional pursuits, I enjoy chatting with my family and friends, visiting new cities, learning about new cultures, languages, food, and life hacks. By the way, where I currently live, Norway, people believe in Trolls, and I do too! This country is a fascinating place full of kind people, breathtaking nature, big fjords, good salmon, Hånsa, deer, and other cool things.

Math research

My research is situated within the field of constructive mathematics and specifically, the study of mathematical constructions within the framework of Homotopy type theory. This relatively recent type theory is particularly noteworthy due to its mathematical interpretation and its structural principles. Arguably, type theories can be defined as formal systems and also as functional programming languages. From this perspective, there is no distinction between the process of proving mathematical statements and programming on a computer, facilitating the assessment of the correctness of mathematical statements.

keywords: dependent type theory, homotopy type theory, agda, functional programing, proof-assistant, univalence axiom, univalent mathematics

You might also be interested in the following projects:

Archived

Other initiatives

Summer Schools/Conferences

Selected talks

Seminar talks

As a member of the PLT group at Heliax, I have contributed with the following talks:

As a member of the Logic and Computation group at Universidad EAFIT, I presented the following talks:

Teaching experience

As a PHD student at UiB, I did TA work for the following courses:

In Colombia, I was the lecturer for the following courses:

Archived software projects

Some no academic-related open-source projects:

Old notes

More information

Check out my CV.


Jonathan Prieto-Cubides's website