A Simplified version of Bitcoin, implemented in Agda

Aluno(a): 

  • Guilherme Horta Alvares da Silva

Data: 

12/03/2020 - 15:00

Local: 

Fundação Getulio Vargas Praia de Botafogo, 190 - sala 308

Resumo: 

Uma criptomoeda é uma moeda digital que funciona de maneira descentralizada, sem uma autoridade central e seus estados são mantidos por meio de consenso distribuído. Ela tem um papel importante na sociedade, porque é um dinheiro que é governado apenas por algoritmos e evita grande centralização de poder, como a de bancos e a do governo. Agda é uma linguagem de programação funcional com tipos dependentes. É também um assistente de prova baseado no paradigma de preposição como tipos, assim como Coq. Essa linguagem é útil para provar propriedades sobre o código. Apresentamos nesse trabalho uma explicação sobre o que são criptomoedas e suas principais características, uma breve explicação sobre o Lambda Calculus, tipos de dependentes e Agda, e apresentamos um modelo de criptomoeda feito nessa linguagem. A maioria das partes do Bitcoin é codificada e programada nesse modelo. Desde transações, árvore de transações, Ledger, bloco e cadeia de blocos. As funções criptográficas, como funções hash, funções de transformação de uma chave privada em uma chave pública e seus endereços, são postuladas. Além disso, neste trabalho, há código que transforma e valida transações de um texto sem formatação para o nosso modelo.

*Texto enviado pelo aluno. 

Membros da banca: 

  • Flávio Codeço Coelho (orientador) - FGV EMAp
  • Alexandre Rademaker - FGV EMAp
  • Alexandre Linhares - FGV EBAPE