Version of Monday, April 12, 2021, 08:42 AM
Powered by pandoc 2.10.1
jonathan.cubides@uib.noWelcome, this is my personal website. I’m from the beautiful country Colombia and the capital city Bogotá. I have two first names and two last names as almost everyone in South America. The first last name is by my father, Rafael Prieto, and the other by my mother, Luzmila Cubides. My full name is Jonathan Steven Prieto Cubides. Nowadays, I live in Norway, a fascinating country full of kind people, breathtaking nature, big fjords, good salmon, hansa, deers, and many other cool things.
I am currently a PhD student in computer science at the University of Bergen in the Deparment of Informatics. My current supervisors are Håkon R. Gylterud and Marc Bezem. 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. For example, my programs usually contain specifications, i.e. lemmas along with their corresponding proofs. Then, one can assess the correctness of the mathematical results with a total level of confidence 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 other academic interests, e.g. natural language processing, machine learning algorithms, algorithm design, philosophy of sciences, programming language theory, and software development.
I am currently working on graph-theoretical constructions using Univalent Foundations. The following address contains a work-in-progress formalisation of this project in the proof-assistant Agda v2.6+.
Metis, only the core for propositional logic.Agda library to work with classical propositional logic based on a deep embedding.TPTP problems and TSTP solutions of problems in classical logic.Agda.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 developement 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.Flask full-text search engine.Python package to make full-text searchable Pony databases.Alloy. June 20, 2017. Universidad EAFIT.I have been teaching assistant for the following courses at University of Bergen:
I taught the following courses:
(2021-04-09) (442e194) [ css ] pic class update. (2021-04-09) (76cd983) [ css ] pic class update. (2021-04-09) (36c6f13) fixed some links (2021-04-09) (5f5bb90) Fixed intro. (2021-04-09) (140a265) [ css ] fixed image max-width.