Uma formalização da teoria nominal em Coq

• Ano de defesa: 2022
• Autor(a) principal: Paranhos, Fabrício Sanches
• Orientador(a): Ventura, Daniel Lima
• Banca de defesa: Ventura, Daniel Lima, Vieira, Bruno Lopes, Nantes Sobrinho, Daniele
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Goiás
• Programa de Pós-Graduação: Programa de Pós-graduação em Ciência da Computação (INF)
• Departamento: Instituto de Informática - INF (RG)
• País: Brasil
• Palavras-chave em Português: Conjuntos nominais; Técnicas nominais; Formalização; Coq
• Palavras-chave em Inglês: Nominal sets; Nominal techniques; Formalization; Coq
• Área do conhecimento CNPq: CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO
• Link de acesso: http://repositorio.bc.ufg.br/tede/handle/tede/12314

In the implementations and analysis of programming languages, the need for manipulation, or demonstration, of terms containing variable binding structures is recurrent. However, in practice, this is not a trivial task. The main problems are the capture of free variables, the identification of α-equivalent terms and inductive demonstrations about terms containing bound variables, in which several variable renaming lemmas are needed. In the informal context, several devices were developed to mitigate problems related to bound variables, such as, for example, the Barendregt Variable Convention. While in the context of proofs verification, formalized in a proof assistant, it is still an open problem with several solutions and proposals for the representation of bound variables. Among them, nominal techniques have been praised for their ability to formalize grammars with binding structures closer to their informal developments, through a uniform metatheory based on name permutation. Due to the lack of a nominal library for constructive proof assistants, we present in this dissertation an ongoing formalization of the nominal theory in Coq, where we highlight the main design and project decisions. We implemented and compared two methods, a pragmatic one, supported by the basic pillars of nominal theory, and a constructive formalization of the main elements of nominal theory: nominal sets, support, freshness, supported functions, nominal α-equivalence and name abstraction. Our main contribution was to present a class hierarchy for the definition of nominal sets, which combined with the generalized rewriting mechanism, achieve concise definitions and proofs, while avoiding the well-known “setoid hell” scenario.