Welcome, this is my personal website.

Contact information

• Email: jonathan.cubides@uib.no
• Office: Institutt for informatikk Postboks 7803, Thormøhlens Gate 55, 5020 Bergen, Norway
• Github: jonaprieto
• Keybase: jonaprieto
• Twitter: jonaprietoc
• Linkedln: jonathan-prieto-cubides

About me

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.

Research work

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.

Academic projects

Active projects

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

  • https://jonaprieto.github.io/synthetic-graph-theory/

• Contribuiting on the formalisation in Agda of the Symmetry Book.

  • https://github.com/UniMath/SymmetryBookFormalization
  • https://unimath.github.io/SymmetryBookFormalization/

Former projects

Projects related to my master

• athena: a proof-reconstruction implementation in type theory for the propositional logic fragment of the automatic theorem prover Metis. (Haskell) (PDF).
• agda-metis: a formalisation of the propositional fragment in Metis.
• agda-prop: a deep embedding specification of classical propositional logic in Agda.
• prop-pack: a collection of TPTP problems and TSTP solutions of problems in classical logic to test automatic provers.
• online-atps: a command-line tool to use popular automatic theorem provers.
• agda-pkg: a simple example of a package-manager for Agda.

Other initiatives

• A reading group on PL topics by graduate students and friends at UiB. See theuibcoworkers.
• Organizer and problem setter for a few programming contests at Universidad Sergio Arboleda.
• Quantum computing seminar for undergrads at Universidad Sergio Arboleda

Summer Schools/Conferences

• 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.
• Agda Implementors’ Meeting XXV in Gothenburg, Sweden, 9-15 May, 2017.

Selected talks

• Investigations on graph-theoretical constructions in HoTT. Univalent Foundations For Daily Application (UFFDA), 18-19 November 2021, Bergen, Norway. (PDF)
• Automatic Theorem Proving, an act of trust. ICT Ph.D Forum, 26-27 October 2020, Voss, Norway,
• Planar Graphs in Univalent Mathematics. TYPES 2019 in Oslo, Norway, 11 June. 2019. (PDF)
• Pathovers, An Introduction to Dependent Type Theory. Lafayette Topology Seminar , 14 December 2018, Lafayette, USA.
• Proof-reconstruction in Agda. Agda Implementors' Meeting XXV 9-15 May 2017, Gothenburg, Sweden.

Seminar talks

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

Teaching experience

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.
• Software 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.

Archived software projects

• arsi: a selection algorithm on rough sets for missing data in databases.
• 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 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.
• hott-cheatsheets: a collection of homotopy type theory cheatsheets with the content of the HoTT Book.

Some no academic-related open-source projects:

• flask-ponywhoosh: a Flask full-text search engine.
• ponywoosh: a Python package to make full-text searchable Pony databases.
• python-atxt: a tool to extract text data from different kind of files. Available upon request.
• dig: a web scrapper with a nice GUI. Available upon request.

Old notes

• The Pigeonhole principle (PDF) (Agda).
• Pathovers.
• Circle equivalences.

More information

Check out my CV.

---

Jonathan Prieto-Cubides's website