Jonathan Prieto-Cubides

Welcome to my personal website!

Contact Information

About Me

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

With over seven 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 was a compiler engineer and product lead also at Heliax AG, working on the Juvix programming language and related compiler projects for Anoma. Prior to that, I was enrolled in a PhD program at the University of Bergen, Norway, where I worked on graph-theoretical constructions in homotopy type theory. I have a master’s degree in Applied Mathematics from Universidad EAFIT, Colombia, where I worked on proof-reconstruction in type theory, and I have a bachelor’s degree in Mathematics from Universidad Sergio Arboleda, Colombia, where I worked on elliptic curves.

Keywords: Formal methods, type theory, logic, algorithms, graph theory, category theory, functional programming, proof-assistant, univalent mathematics.

Work Experience

Research & Development Engineer, Heliax AG

Compiler Engineer & Product Lead, Heliax AG

Previous Work Experience

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.

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

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

Other universities I have attended:

Summer Schools/Conferences
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

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

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

Jonathan Prieto-Cubides's website