Last updated: September 25, 2025
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.
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.Elixir
, Rust
, and GitHub Actions CIAnoma 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.
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
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
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
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 in Applied Mathematics - Logic and Algorithms, Universidad EAFIT
Metis
.Agda
.TPTP
problems
and TSTP
solutions of problems in classical logic to test automatic provers.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 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
full-text search engine.Python
package to make full-text searchable Pony
databases.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!