Utilize este link para identificar ou citar este item: https://bdm.unb.br/handle/10483/41008
Arquivos neste item:
Arquivo Descrição TamanhoFormato 
2024_JoseRSoares_tcc.pdf384,57 kBAdobe PDFver/abrir
Título: Formalização em Coq da prova de confluência do cálculo λx no contexto nominal
Autor(es): Soares, José Roberto
Orientador(es): Moura, Flávio Leonardo Cavalcanti de
Assunto: Linguagem de programação (Computadores)
Cálculo lambda
Data de apresentação: 14-Out-2024
Data de publicação: 18-Dez-2024
Referência: SOARES, José R.. Formalização em Coq da prova de confluência do cálculo λx no contexto nominal. 2024. 39 f. Trabalho de Conclusão de Curso (Bacharelado em Engenharia da Computação) — Universidade de Brasília, Brasília, 2024.
Resumo: O cálculo λ é amplamente reconhecido no meio acadêmico como um modelo fundamen tal da computação, servindo como base para o paradigma funcional, que é a essência de linguagens de programação como Haskell, Lisp e OCaml. Além dessas, diversas out ras linguagens, como Python, JavaScript e C++, incorporam conceitos do paradigma funcional de maneira indireta, permitindo a combinação de estilos de programação fun cionais e imperativos. A propriedade de confluência assegura ao cálculo o determinismo e confiabilidade no sistema, afirmando que, a partir de qualquer divergência realizada no cálculo (através das operações de redução), o resultado final irá convergir para o mesmo ponto em comum. Existem várias formas de formalização da propriedade de confluên cia, e a escolhida neste trabalho foi através da propriedade propriedade Z composicional, detalhada em [1]. Neste trabalho, estudaremos esta propriedade em uma extensão do cálculo λ chamada de cálculo λx, que conta com um construtor de substituição explícita, desta forma, se aproximando mais das linguagens de alto nível puramente funcionais. A formalização foi feita utilizando o assistente de provas Coq, uma poderosa ferramenta para verificação formal de teoremas, permitindo uma descrição rigorosa e garantindo a correção dos resultados obtidos. Este trabalho tem como objetivo expandir o framework para o estudo de propriedades de cálculos com substituições explícitas no contexto nominal. Como aplicação, utilizamos o cálculo λx através do assistente de provas Coq. O código pode ser encontrado no repositório [2].
Abstract: The lambda calculus is widely recognized in academia as a fundamental model of com putation, serving as the foundation for the functional paradigm, which is the essence of programming languages such as Haskell, Lisp, and OCaml. In addition to these, several other languages, such as Python, JavaScript, and C++, incorporate functional paradigm concepts indirectly, allowing for the combination of functional and imperative program ming styles. The confluence property ensures determinism and reliability in the system, asserting that from any divergence that occurs in the calculus (through reduction opera tions), the final result will converge to the same common point. There are several ways to formalize the confluence property, and the one chosen in this work was through the compositional property Z, detailed in [1]. In this work, we will study this property in an extension of the lambda calculus called λx calculus, which includes an explicit substi tution constructor, thereby getting closer to purely functional high-level languages. The formalization was done using the Coq proof assistant, a powerful tool for formal theorem verification, allowing for rigorous description and ensuring the correctness of the results obtained. This work aims to expand the framework for studying properties of calculi with explicit substitutions in the nominal context. As an application, we prove the confluency property of the λx calculus with the use of the Coq proof assistant. The code can be found in the repository [2].
Informações adicionais: Trabalho de Conclusão de Curso (graduação) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2024.
Licença: A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta.
Aparece na Coleção:Engenharia da Computação



Todos os itens na BDM estão protegidos por copyright. Todos os direitos reservados.