Welcome to my personal website!
jonathan.cubides@uib.no
, prieto.jona@gmail.com
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.
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
An abstract of the project is here: graph-theoretical
constructions
expressed in Univalent
Mathematics. The
following URL address contains a work-in-progress formalisation on
this topic. The proofs are type-checked with the proof assistant Agda
v2.6.2. Feel free to email me if you are working on similar topics and
are interested in discussing anything.
You might also be interested in the following projects:
Metis
.Agda
.TPTP
problems
and TSTP
solutions of problems in classical logic to test automatic provers.Agda
.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:
As a PHD student at UiB, I did TA work for the following courses:
In Colombia, I was the lecturer for the following courses:
Mathematica
, designed for retrieval, analysis and
systematization of large textual data (in the order of tens of
thousands of files). Poirot is tailored for the needs of qualitative
researchers, journalists, and state officials (in the judiciary, for
example), that need to find specific textual bits in big masses of
unstructured text. This development was part of a larger project by
Observatorio de Restitución de
Tierras and Universidad
Sergio Arboleda, both Colombian research organizations. Therefore,
the source code is private, but if you are interested in, you can
contact me.Some no academic-related open-source projects:
Flask
full-text search engine.Python
package to make full-text searchable Pony
databases.Check out my CV.