Version of Monday, April 12, 2021, 08:42 AM

Powered by pandoc 2.10.1

**Email:**`jonathan.cubides@uib.no`

**Office:**Institutt for informatikk Postboks 7803, Thormøhlens Gate 55, 5020 Bergen, Norway**Github:**jonaprieto**Keybase:**jonaprieto**Twitter:**jonaprietoc

Welcome, 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+.

- athena: proof-reconstruction in type theory for propositional logic. (PDF).
- agda-metis: a formalisation of the reasoning used in the theorem prover
`Metis`

, only the core for propositional logic. - agda-prop: an
`Agda`

library to work with classical propositional logic based on a deep embedding. - prop-pack:
`TPTP`

problems and`TSTP`

solutions of problems in classical logic. - online-atps: command-line tool to use popular automatic theorem provers.
- agda-pkg: a package-manager for
`Agda`

.

- hott-cheatsheets: homotopy type theory cheatsheets to read the HoTT Book
- arsi: dealing with missing data using a selection algorithm on rough sets.
*poirot*: a text search, a package, and analysis platform programmed in`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-ponywhoosh: a
`Flask`

full-text search engine. - ponywoosh: a
`Python`

package to make full-text searchable`Pony`

databases. - python-atxt: extract text data from different kind of files.
- curriculum-vitae: a pandoc template for writing Resumés

- theuibcoworkers: reading group on PL topics by graduate students and friends at UiB. We usually meet twice per week, if you want to join us, contact me.
- Organizer of a few programing contests at Universidad Sergio Arboleda
- Undergraduate seminar of quantum computing at Universidad Sergio Arboleda

- Midlands Graduate School (MGS) in Cyberspace, 12-16 April 2021.
- UiB ICT Ph.D Forum in Voss, Norway, 26 October, 2020.
- HoTT Summer School in Pittsburgh, USA, August. 2019.
- TYPES 2019 in Oslo, Norway, June. 2019.
- Midlands Graduate School (MGS) at University of Birmingham, UK, April, 2019.
- EUTypes Summer School in Ohrid, Macedonia, 8-12 August, 2018.
- Agda Implementors' Meeting XXVII in Gothenburg, Sweden, 4-9 June, 2018.

- Automatic theorem proving, an act of trust. ICT Ph.D Forum in Voss, Norway, 26 October, 2020.
- Planar graphs in univalent mathematics. TYPES 2019 in Oslo, Norway, 11 June. 2019. (PDF)
- An introduction to dependent type theory. Lafayette Topology Seminar in Lafayette, USA, 14 December, 2018.
- Proof-reconstruction in Agda. Agda Implementors' Meeting XXV in Gothenburg, Sweden, 9-15 May, 2017.

- Model checking with
`Alloy`

. June 20, 2017. Universidad EAFIT. - Simple typed lambda calculus. 2017. Universidad EAFIT.
- Kripke semantics. Logic and Computation group seminar, 2016. Universidad EAFIT.

I have been teaching assistant for the following courses at University of Bergen:

- Introduction to logic, Spring 2020.
- Concurrent programming, Fall 2018, 2019, and 2020.
- Models of computation, Spring 2019.
- Sofware engineering, Spring 2018.

I taught the following courses:

- Linear algebra, Instituto Técnologico Metropolitano, Medellín, Colombia, 2016.
- Discrete matematics, Universidad Sergio Arboleda, Bogotá, Colombia, 2014.
- Algorithms I and II, Universidad Sergio Arboleda, Bogotá, Colombia, 2013-14.

- Pathovers.
- Circle equivalences.
- The Pigeonhole principle (PDF) (Agda code).

(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.