Welcome, this is my personal website.
jonathan.cubides@uib.no
I am a Colombian researcher and explorer from the capital city Bogotá, mostly into mathematics and computer science. In addition, I enjoy visiting new cities and learning about new cultures, languages, food, and life in general.
Where I live, people believe in Trolls, and I do too! Norway is a a fascinating country full of kind people, breathtaking nature, big fjords, good salmon, Hansa, deer, and other cool things.
As a remark, my full name is Jonathan Steven Prieto Cubides. My first last name is by my father, Rafael A. Prieto B., and the other by my mother, Luzmila Cubides.
Nowadays, I am a PhD Candidate in computer science at the University of Bergen in the Department of Informatics. My supervisors are Håkon R. Gylterud and Marc Bezem. I share my office with Benjamin Chetioui and Tam Thanh Truong.
The context of my research is within the field of constructive mathematics. I study mathematical constructions within a relatively recent type theory called homotopy type theory. Many type theories have computational meaning, making them practical to use for computing. A type theory can be defined as a formal system and also as a functional programming language. In this view, there is, therefore, no distinction between doing mathematics as proving statements and programming on the computer. As a consequence, one can assess the correctness of the mathematical results produced using this approach, up to the correctness of the proof-checker.
keywords: dependent type theory, homotopy type theory, agda, functional programing, proof-assistant, univalence axiom, univalent mathematics
I have more academic interests, e.g. natural language processing, machine learning algorithms, algorithm design, philosophy of sciences, programming language theory, and software development.
The most active project is on graph-theoretical
constructions
expressed in Univalent
Mathematics. The
following URL address contains my 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 or
you are interested in discussing any related topic.
Contribuiting on the formalisation in Agda of the Symmetry Book.
Metis
.Agda
.TPTP
problems
and TSTP
solutions of problems in classical logic to test automatic provers.Agda
.I have been teaching assistant for the following courses at University of Bergen:
I taught 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.