Aluno-pesquisador:
Henrique Borges Carvalho
Orientador:
- Professor Alexandre Rademaker
Ano:
2025
Escola:
- EMAp - Escola de Matemática Aplicada
Este projeto tem como objetivo a adaptação da biblioteca de visualização Vizagrams.jl para o ambiente Lean. A biblioteca original, desenvolvida por Davi Sales Barreira, baseia-se em conceitos fundamentais da teoria de categorias, com especial ênfase no artigo Monoids: Theme and Variations (Functional Pearl). Nossa abordagem busca implementar as funcionalidades essenciais da Vizagrams.jl dentro do ecossistema Lean4, garantindo 100% de compatibilidade com a implementação original e pretende ser a primeira biblioteca de visualização para a linguagem Lean.