Proyectos
A = Autor, CA = Coautor, C = Contribuidor
Blockchain & EVM
- anoma-explorer A (2026) – Block explorer para Anoma desarrollado con Elixir/Phoenix LiveView.
- anoma-envio A (2026) – Indexador en TypeScript/GraphQL para eventos de Anoma.
- anoma-swap CA (2026) – Interfaz de token swap para Anoma: frontend en Phoenix + backend en Rust con ZK proofs para la lógica de la Resource Machine.
- pa-evm C (2026) – Protocol Adapter que conecta la Anoma Resource Machine con Ethereum y Arbitrum. Solidity/Rust.
- anomapay-erc20-forwarder C (2026) – Contrato ERC-20 Forwarder para AnomaPay. Solidity.
- toyevm A (2026) – Un tutorial de 7 días basado en ejercicios para construir una Ethereum Virtual Machine desde cero en Rust. (work in progress)
Distributed Systems & Protocols
- mailbox-actors A (2025) – Modelo formal de sistemas de actors basados en mailboxes en Lean 4: semántica de actors, entrega de mensajes y composición de sistemas. Documentación
- avm-lab A (2025) – Anoma Virtual Machine: especificación formal en Agda e implementación en Rust con interaction trees, ejecución transaccional y análisis de control flow.
- engine A (2023-2025) – Biblioteca en Elixir que implementa la arquitectura del Anoma engine: OTP supervision tree, GenStage messaging y DSL validado en compile time.
- dexes A (2025) – HyperCow: prototipo de decentralized exchange basado en SPEEDEX sobre Anoma (Elixir). Más de 60 PRs.
- tango A (2024) – Biblioteca de estructuras de datos replicadas in-memory en Elixir.
- nspec CA (2023-2025) – Tooling de especificación de Anoma e infraestructura MkDocs. Más de 100 PRs.
- art CA (2023-2025) – Índice de Anoma Research Topics: template en LaTeX, edición de papers y sistema de publicación en Zenodo.
Compiler & Language Tooling
- juvix CA (2021-2023) – Lenguaje de functional programming para aplicaciones descentralizadas intent-centric. Lideré la dirección de producto y envié más de 50 PRs de compiler en Haskell.
- vscode-juvix A (2021-2023) – Extensión de VS Code para Juvix: syntax highlighting, REPL, CodeLens, hover/typecheck. Más de 50 releases.
- juvix-mkdocs A (2023) – Plugin de MkDocs para literate programming con Juvix y type checking en build time.
- juvix-docs A (2022-2023) – Fuente de documentación de docs.juvix.org.
- juvix-stdlib CA (2022-2023) – Standard library de Juvix y configuración de CI.
- juvix-containers A (2022) – Contenedores Docker para CI de Juvix.
- homebrew-juvix A (2022) – Homebrew tap para distribución de Juvix en macOS.
- vamp-ir C (2022) – Automatización de releases para este lenguaje de zero-knowledge circuits (Rust).
Formal Verification & Proof Assistants
- athena A (2017) – Traduce la salida de pruebas del ATP Metis a código compilable en Agda. Haskell.
- online-atps A (2017) – CLI para automated theorem provers remotos vía SystemOnTPTP. Haskell.
- agda-metis A (2017) – Formalización en Agda de los pasos de razonamiento del prover Metis.
- agda-prop A (2017) – Biblioteca de lógica proposicional clásica en Agda.
- agda-pkg A (2018-2020) – Package manager para Agda.
- agda-unimath C (2020) – 8 PRs mergeados mejorando el sitio de documentación.
- apia C (2016-2017) – Proyecto de proof reconstruction en Haskell.
- HoTT-Book C (2019) – Correcciones y contribuciones al libro de HoTT.
- plfa.github.io C (2019) – Programming Language Foundations in Agda.
Otros
- agda-mode-vscode C (2021) – Agda mode para VS Code.
- hott-cheatsheets A (2019) – Cheatsheets comunitarios para el libro de HoTT. LaTeX.
- flask-ponywhoosh A (2015) – Extensión de Flask que integra PonyORM con Whoosh para full-text search. Python.
- ponywhoosh A (2015) – Full-text search con PonyORM vía Whoosh. Python.
- python-atxt A (2015) – Herramienta para extraer texto de distintos formatos de archivo. Python.
- prop-pack A (2017) – Colección de problemas TPTP y soluciones TSTP para testing de automated provers.
- arsi A (2014-2016) – Algoritmo de selección sobre rough sets para datos faltantes. Mathematica.
- poirot A (2014-2016) – Plataforma de búsqueda y análisis de texto en Mathematica para datos textuales a gran escala. Desarrollado para el Observatorio de Tierras. Código fuente privado.