Welcome to my personal website!

Contact Information

• Email: jonathan.cubides@uib.no, prieto.jona@gmail.com
• GitHub: jonaprieto
• Twitter: jonaprietoc
• LinkedIn: jonaprieto
• Homepage: jonaprieto.github.io
• ORCID: 0000-0002-8449-3812

About Me

Hola! I’m a Colombian researcher and explorer from the capital city Bogotá.

With a few years of experience as a research engineer, I have developed a diverse skill set specializing in mathematical conceptualization, research, and product development across various technologies and domains. Currently, I am working as a research engineer at Heliax AG on the Anoma specification, an Actor-like model theory for Anoma, and the Anoma research topics index. Before this, I worked as a compiler engineer and product lead on the Juvix programming language and related compiler projects for Anoma, also at Heliax AG. I did my PhD at the University of Bergen, where I worked on graph-theoretical constructions in homotopy type theory. I have a master’s degree in Applied Mathematics from Universidad EAFIT, where I worked on proof-reconstruction in type theory and automated theorem proving. I have a bachelor’s degree in Mathematics from Universidad Sergio Arboleda, Colombia.

Keywords: Formal methods, type theory, logic, algorithms, graph theory, category theory, functional programming, proof assistants, univalent foundations, constructive mathematics, mathematical formalization, graphs, surfaces, planar graphs, trees, compilers, programming languages, formal verification,

Work Experience

Research & Development Engineer, Heliax AG

• Jan 2023 - Present. Remote.
• Specification & Anoma Research Topics’ Editor
  • Anoma Specs
  • Anoma Research Topics Art
  • ART Anoma

Compiler Engineer & Product Lead, Heliax AG

• Mar 2022 - Dec 2023. Remote.
• Juvix Programming Language and Related Compiler Stack Projects
  • Juvix Docs
  • Juvix GitHub

Researcher, Heliax AG

• Aug 2021 - Mar 2022. Remote.

As Compiler Team Member (part-time), I contributed with the following talks:

• Two-level type theory for metaprogramming. 2022. PLT seminar.
• Termination checker strategies. 2022. PLT seminar.
• An internalist approach to correct-by-construction compilers. 2021. PLT seminar.
• Bidirectional type checking algorithms. 2021. PLT seminar.
• HoTT day in Berlin. 2021. PLT seminar.
• Typechecking for STLC in Agda. 2021. PLT seminar.

Previous Work Experience

Teaching Assistant, Department of Informatics, University of Bergen

• 2018-2021. Bergen, Norway.
• Master courses: Models of Computation, Concurrent Programming, Introduction to Logic, Software Engineering

Young Research Assistant, Department of Mathematics, Universidad EAFIT

• 2016-2017. Medellín, Colombia.
• Contributed to the Apia Haskell Project and developed a tool called Online-ATPs.

Lecturer, Instituto Tecnológico Metropolitano

• July 2016 - Dec 2016. Medellín, Colombia.
• Undergraduate courses: Linear Algebra, Linear Programming, and Algebra

Machine Learning Engineer, Observatorio de Tierras

• 2014 - 2016. Bogotá, Colombia.
• Developed ML algorithms and text data mining tools.

Lecturer, Universidad Sergio

• 2012-2014. Bogotá, Colombia.
• Undergraduate courses: Algorithms I-II, Discrete Mathematics

Full-stack Python Developer, Vanitech

• 2012-Bogotá, Colombia.
• Developed the booking platform and landing page.

Software Developer, Scripta Software

• 2009-Bogotá, Colombia.
• Implemented the RSA algorithm for a C# .NET API to serve encryption/decryption services integrated into a financial tool.

---

Education

• PhD in Computer Science, Informatics, ICT Research Group, University of Bergen

  • 2018 - 2023. Bergen, Norway. Defended on December 15, 2024.

  • Thesis title: Investigations into Graph-Theoretical Constructions in Homotopy Type Theory.

    Abstract

    This thesis presents a novel constructive and proof-relevant development of graph theory concepts within Homotopy Type Theory (HoTT). HoTT, an extension of Martin-Löf’s intuitionistic type theory, incorporates novel features like Voevodsky’s Univalence principle and higher inductive types. Its structuralist perspective aligns with standard mathematical practise by promoting isomorphisms to equalities — inhabitants of the corresponding Martin-Löf’s identity type. This thesis primarily delves into the foundational mathematics of graphs, with less emphasis on their practical aspects. The core contributions are definitions, lemmas, and proofs, which often arise from a synthesis of informal presentation and formalisation within a proof assistant. We specifically work within the category of directed multigraphs in HoTT.

    Inspired by the topological and combinatorial facets of graphs on surfaces, we formulate an elementary characterisation of planar graphs. This is done without defining a surface or directly working with real numbers, as found in some literature. Our approach hinges on graph maps and faces for locally directed and connected multigraphs. A graph qualifies as planar if it features a graph map and an outer face, allowing any walk in the embedded graph to be merely walk-homotopic to another.

    Among our key discoveries, we ascertain that this kind of planar maps constitutes a homotopy set, which is finite when the graph is finite. Additionally, we introduce extensions of planar maps to inductively generate examples of planar graphs. We also delve into further concepts such as spanning trees and higher dimensional representations of graphs as spaces through graph maps.

    • PDF
    • Slides
    • Agda code and other related sources.

  • Supervisors: Håkon R. Gylterud and Marc Bezem.

  • Interests: type theory, logic, algorithms, graph theory, category theory

  • Talk on Modal logics and Kripke semantics

  • Motivation

    My PhD 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. This is facilitated by the proof-assistant tools, which allow the user to write proofs in a formal language and check their correctness.

    Keywords: dependent type theory, homotopy type theory, agda, functional programming, proof-assistant, univalence axiom, univalent mathematics

• M.Sc. in Applied Mathematics - Logic and Algorithms, School of Sciences, Universidad EAFIT

  • 2016 - 2017. Medellín, Colombia. Defended on December, 2017.
  • Thesis title: Proof-Reconstruction in Type Theory for Propositional Logic.
  • Supervisor: Andrés Sicard-Ramírez.
  • Interests: type theory, functional programming, proof-assistant, automated theorem proving.

• B.Sc. in Mathematics, Faculty of Engineering, Universidad Sergio Arboleda

  • 2007 - 2013. Bogotá, Colombia.
  • Thesis title: Introduction to Elliptic Curves, and the Mordel’s theorem.
  • Supervisor: Hermés Martínez.

Other universities I have attended:

• Universidad Nacional de Colombia (2009-2013) - Economics & Systems Engineering - Bogotá, Colombia. Dropout.

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.

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

As a member of the Logic and Computation group at Universidad EAFIT, I presented the following talks:

• Proof-reconstruction in Agda. 2017. Logic and Computation group seminar, Universidad EAFIT.
• 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.

Publications

• Prieto‐Cubides, Jonathan and Håkon Robbestad Gylterud (2024). On planarity of graphs in homotopy type theory. Mathematical Structures in Computer Science, pp. 1–41. DOI: 10.1017/S0960129524000100.
• • (2024). Artefact: Mechanised proofs in Agda for the manuscript “Investigations into Graph‐theoretical Constructions in Homotopy Type Theory”. DOI: 10.5281/zenodo.11092174.
• – (2022). On Homotopy of Walks and Spherical Maps in Homotopy Type Theory. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2022. Philadelphia, PA, USA: Association for Computing Machinery, pp. 338–351. DOI: 10.1145/3497775.3503671.
• Prieto‐Cubides, Jonathan and Camilo Argoty (2018). Dealing with Missing Data using a Selection Algorithm on Rough Sets. International Journal of Computational Intelligence Systems 11.1, p. 1307. DOI: 10.2991/ijcis.11.1.97.
• Prieto‐Cubides, Jonathan (2017). Proof‐Reconstruction in Type Theory for Propositional Logic. Master’s Thesis. DOI: http://doi.org/10.5281/zenodo.1127672.

Music

When teenage, I played the guitar and enjoyed listing to Thrash and Power metal. Nowadays, I can listen to almost any genre, mostly by friend’s recommendations, including rap, hip-hop, and classical music.

Hobbies

When not working, I enjoy chess, and video games. I also like to do nothing every once in a while.

Other Stuff

Archived Software projects

• athena: a proof-reconstruction implementation in type theory for the propositional logic fragment of the automatic theorem prover Metis. (Haskell) (PDF).
• online-atps: a command-line tool to use popular automatic theorem provers.
• 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.
• agda-pkg: a simple example of a package-manager for Agda.
• hott-cheatsheets: a collection of homotopy type theory cheatsheets with the content of the HoTT Book.
• 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.

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.

Community initiatives

• ICFP 2024 Artifact Evaluation Committee
• 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

Short Notes

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

For more detailed information, please refer to my full CV.

---

Jonathan Prieto-Cubides's website