Detalhes bibliográficos
| Ano de defesa: |
2020 |
| Autor(a) principal: |
Silva, Guilherme Horta Alvares da |
| Orientador(a): |
Coelho, Flávio Codeço |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
eng |
| Instituição de defesa: |
Não Informado pela instituição
|
| Programa de Pós-Graduação: |
Não Informado pela instituição
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Não Informado pela instituição
|
| Palavras-chave em Português: |
|
| Link de acesso: |
https://hdl.handle.net/10438/29110
|
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. |
