A Simplified version of Bitcoin, implemented in Agda

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.

Ficha do documento

Tipo

Dissertação

Ano

2020

Instituição

Fundação Getulio Vargas

Fonte

Repositório da FGV

Idioma

Inglês

Acesso

Não informado

Identificador

oai:repositorio.fgv.br:10438/29110

Temas

TecnologiaDados

Palavras-chave

VerificationFormal methodsAgdaSmart contractBlockchainCryptocurrencyBitcoinBitcoin - Modelos matemáticosBlockchains (Base de dados)Agda (Linguagem de programação de computador)Transferência eletrônica de fundosMoeda