Last updated: September 25, 2025

About me

Hola! I’m a R&D Engineer originally from Bogotá, passionate about exploring knowledge at the intersection of mathematics and computer science. I specialize in technology backed by solid mathematical foundations, with particular enthusiasm for formal verification and raising AI systems that enhance reasoning capabilities.

I have experience in mathematical conceptualization, compiler development, and protocol design. I consider myself a flexible and adaptable engineer, always looking for new challenges and opportunities to learn. Get in touch with me if you want to discuss a project or collaboration.

prieto.jona@gmail.com | LinkedIn | GitHub | ORCID | CV PDF.

Work Experience

R&D Engineer | Heliax AG | September 2025 - Present
  • TBD
Elixir Developer | Heliax AG | June - September 2025
  • The company wanted to build a prototype of a vault-based exchange for the Anoma network implementing Speedex batch-processing algorithm. I use Elixir to implement the exchange, learned about market order types, batch-processing, and modelling different data types to be used in the exchange. And carrying out the implementation in Elixir with Anoma Elixir guidelines.
  • Tech stack: Elixir, Rust, and GitHub Actions CI
R&D Engineer | Heliax AG | Jan 2023 - June 2025
  • Extended protocol specification and research documentation for Anoma ecosystem
  • Key deliverables:
    • Anoma Protocol Specification, where I learned about different actor models and protocol desing. In particular, I contributed with the design of the Anoma engine theoretical framework for distributed systems, and the mailbox architecture.

    • Research Topics Index - I helped creating the index, reviewing a few research papers and contributing writing or copy-editing some of the papers.

    • Engine Library - I wrote the core Elixir implementation that adheres to the Anoma engine architecture. I use AI to help me with the implementation.

    • Similarly, in Tango - I implemented from reading the Tango paper and using AI, a proof-of-concept of an Elixir library for in-memory replicated data structures for distributed systems.

Haskell Engineer & Product Lead | Heliax AG | Mar 2022 - Dec 2023
  • Led end-to-end development of Juvix, a functional programming language for smart contracts
  • Delivered compiler toolchain, documentation, and developer ecosystem
  • Tech stack, during this period I learned about Haskell and how to carry out a Haskell-project, use Docker for CI images and testing, use GitHub Actions for CI/CD pipelines. Create a Homebrew formula for the Juvix compiler. I also learned how to make a Plugin for the VSCode editor to interact with the Juvix compiler, and got experience in technical writing for the Juvix Project, see juvix.org.
Part-time R&D Engineer | Heliax AG | Aug 2021 - Mar 2022
  • I investigated a proof-of-concept of a usage-aware type theory for the Juvix compiler, learning from the literature in QTT and reporting my findings to the team.
  • Contributed to PLT seminar series on type theory, correct-by-construction compilers in Agda, Two-level type theory for formal specification, termination checking for the Juvix compiler, bidirectional typing for a better type inference for the Juvix compiler, and HoTT for fun.
Teaching Assistant | University of Bergen | 2018-2021
  • 2018-2021 | Bergen, Norway
  • Graduate courses: Models of Computation, Concurrent Programming, Introduction to Logic, Software Engineering
Research Assistant | Universidad EAFIT | 2016-2017
Lecturer | Instituto Tecnológico Metropolitano | 2016-2017
  • July - Dec 2016 | Medellín, Colombia
  • Undergraduate courses: Linear Algebra, Linear Programming, Algebra
Machine Learning Engineer | Observatorio de Tierras | 2014-2016
  • 2014 - 2016 | Bogotá, Colombia
  • Developed ML algorithms and text data mining tools in Mathematica. During this project I learned how to develop a full-text search engine with an inverted index, regular expressions in interaction with big lexicons, and verification of logical expressions in big textual data. Also, implemented Naive Bayes classifier for text classification for Twitter data.
Math Lecturer | Universidad Sergio Arboleda | 2012-2014
  • 2012-2014 | Bogotá, Colombia
  • Undergraduate courses: Algorithms I-II, Discrete Mathematics
Full-stack Python Developer | Vanitech | 2012
  • 2012 | Bogotá, Colombia
  • Developed booking platform and landing page in Python with Flask and SQLite. I learned in this project how to use Flask, SQLite, and how to deploy a web application.
C# Software Developer | Scripta Consulting | 2009
  • 2009 | Bogotá, Colombia
  • Implemented RSA encryption/decryption API in C# .NET for financial applications. I learned how to adapt an isolated solution into a complex enterprise solution.

Here are some of the projects I have contributed to:

juvix | homebrew-juvix | juvix-mkdocs | vscode-juvix | juvix-stdlib | juvix-docs | juvix-containers | vamp-ir | nspec | dexes | engine | art | tango | apia | agda-unimath | agda-mode-vscode | HoTT-Book | plfa.github.io | agda | online-atps | athena | metis | flask-ponywhoosh | ponywoosh | python-atxt

Education

PhD in Computer Science - Type theory and formal verification | University of Bergen | 2018-2023
  • PhD in Computer Science, University of Bergen

    • 2018 - 2023 | Bergen, Norway | Defended December 15, 2023

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

    • 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

MSc. Applied Mathematics - Logic and Algorithms | Universidad EAFIT | 2016-2017
Math bachelor's degree | Universidad Sergio Arboleda | 2007-2013
  • 2007 - 2013 | Bogotá, Colombia
  • Thesis: Introduction to Elliptic Curves and Mordell’s Theorem
  • Supervisor: Hermés Martínez
Economics & Systems Engineering | Universidad Nacional de Colombia | 2009-2013
  • Dropped out in favor of the math bachelor’s degree.

Summer Schools/Conferences

Talks

Publications

Community initiatives

Extra

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.
Short Notes
Hobbies
  • I discovered bouldering thanks to my Bergen friends and even though, I didn’t practice it a lot, since I moved to Bogotá I enjoy it a lot and you can find me climbing at Gran Pared and local Bogotá gyms like Trepa. Lots of fun.

  • Tennis: I also play tennis with my wife weekly at Compensar, nice courts.

  • FPS gaming: I play FPS gaming (Battlefield sniper main).

  • Chess: I play chess occasionally, heavy on some seasons of the year. However, I must confess it’s quite addictive so I don’t play often.

That’s all folks!


Jonathan Prieto-Cubides's website