Compiling general recursive functions into finite depth pattern matching.

dc.contributor.advisorRibeiro, Rodrigo Geraldopt_BR
dc.contributor.authorAmaro, Maycon José Jorge
dc.contributor.refereeRibeiro, Rodrigo Geraldopt_BR
dc.contributor.refereeVieira, Bruno Lopespt_BR
dc.contributor.refereeReis, Leonardo Vieira dos Santospt_BR
dc.date.accessioned2023-03-16T19:22:35Z
dc.date.available2023-03-16T19:22:35Z
dc.date.issued2023pt_BR
dc.descriptionPrograma de Pós-Graduação em Ciência da Computação. Departamento de Ciência da Computação, Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto.pt_BR
dc.description.abstractProgramming languages are popular and diverse, and the convenience of extending or changing the behavior of complex systems is attractive even for the systems with stringent security requirements, which often impose restrictions on the programs. A very common restriction is that the program must terminate, which is very hard to check in general because the Halting Problem is undecidable. In this work, we proposed a technique to unroll recursive programs in functional languages to create terminating versions of them. We prove that our strategy is total and we also formalize term generation and run property- based tests to build confidence that the semantics is preserved through the transformation. This strategy can be used to compile general purpose functional languages to targets such as the eBPF and smart contracts for blockchain networks.pt_BR
dc.description.abstractenLinguagens de programação são populares e diversas, e a conveniência de estender o comportamento de sistemas complexos é atrativo mesmo para aqueles com rígidos requisitos de segurança, que frequentemente impõem restrições aos programas. Uma restrição comum é a de que o programa deve terminar, o que é impossível de se verificar no caso geral, devido à indecidibilidade do Problema da Parada. Neste trabalho, é proposta uma técnica para desenrolar funções recursivas em linguagens funcionais para criar versões terminantes delas. É provado que essa estratégia é total e é formalizada a geração ́ de termos aleatórios, que possibilitam a execução de testes baseados em propriedades para construir confiança de que a semântica é preservada na transformação das funções. A técnica proposta pode ser usada para compilar linguagens funcionais de propósito geral para eBPF, contratos inteligentes de redes de blockchain e outros alvos igualmente restritivos.pt_BR
dc.identifier.citationAMARO, Maycon José Jorge. Compiling general recursive functions into finite depth pattern matching. 2023. 37 f. Dissertação (Mestrado em Ciência da Computação) - Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto, Ouro Preto, 2023.pt_BR
dc.identifier.urihttp://www.repositorio.ufop.br/jspui/handle/123456789/16368
dc.language.isoen_USpt_BR
dc.rightsabertopt_BR
dc.rights.licenseAutorização concedida ao Repositório Institucional da UFOP pelo(a) autor(a) em 04/03/2023 com as seguintes condições: disponível sob Licença Creative Commons 4.0 que permite copiar, distribuir e transmitir o trabalho, desde que sejam citados o autor e o licenciante.pt_BR
dc.rights.urihttp://creativecommons.org/licenses/by-sa/3.0/us/*
dc.subjectRecursionpt_BR
dc.subjectLambda calculuspt_BR
dc.subjectProgram transformationpt_BR
dc.titleCompiling general recursive functions into finite depth pattern matching.pt_BR
dc.title.alternativeCompilando funções recursivas em casamento de padrão finito.pt_BR
dc.typeDissertacaopt_BR

Arquivos

Pacote original

Agora exibindo 1 - 1 de 1
Nenhuma Miniatura Disponível
Nome:
DISSERTAÇÃO_CompilingGeneralRecursive.pdf
Tamanho:
476.18 KB
Formato:
Adobe Portable Document Format
Descrição:

Licença do pacote

Agora exibindo 1 - 1 de 1
Nenhuma Miniatura Disponível
Nome:
license.txt
Tamanho:
1.71 KB
Formato:
Item-specific license agreed upon to submission
Descrição: