Skip navigation
Por favor, use este identificador para citar o enlazar este ítem: http://repositorio.unb.br/handle/10482/7685
Ficheros en este ítem:
Fichero Descripción Tamaño Formato  
2010_WashingtnLuisRibeirodeCarvalhoSegundo.pdf516,71 kBAdobe PDFVisualizar/Abrir
Título : Verificação de propriedades do cálculo גex em Coq
Autor : Carvalho Segundo, Washington Luís Ribeiro de
Orientador(es):: Moura, Flávio Leonardo Cavalcanti de
Assunto:: Verificação formal
Cálculos de substituições explícitas
Cálculo ג
Cálculo ex
Fecha de publicación : 11-may-2011
Citación : CARVALHO SEGUNDO, Washington Luís Ribeiro de. Verificação de propriedades do cálculo גex em Coq. 2010. 71 f. Dissertação(Mestrado em Informática)-Universidade de Brasília, Brasília, 2010.
Resumen : O cálculo גex representa uma solução importante dentro da classe de cálculos de substituições explícitas que lidam com “nomes”, em oposição aqueles que codificam suas variáveis por índices. Delia Kesner obteve, através de um conjunto de provas construtivas, demonstrações das importantes propriedades do גex. Dentre elas, destacamos a PSN, isso é, a Preservação da Normalização Forte, cuja demonstração faz uso de uma estratégia de redução perpétua, que permitiu uma caracterização indutiva do conjunto SN גex. Estendemos a especificação em Coq, já realizada para o cálculo ג, de B. Aydemir et al, e que utiliza lógica nominal para construção de princípios de indução e recursão _-estrutural. Dessa forma nossa especificação inclui a substituição explícita (s[x=t]) na gramática de termos. Avançamos definindo os sistemas de reescrita e as relações de redução do גex, e concluímos por formalizar alguns resultados para o cálculo, a saber: a FC (Composição Completa), a SIM (Simulação de um passo da β-redução) e ainda outros que caminham para a formalização da PSN. _______________________________________________________________________________ ABSTRACT
The גex-calculus represents an important solution among all the class of explicit substitutions calculi that deal with "names", as opposed to those that encode variables by indices. Delia Kesner developed the proofs, through a set of constructive ones, of important properties of the _ex calculus. Among them, we highlight the PSN property, that is, the Preservation of Strong Normalization, whose proof uses a perpetual reduction strategy which allowed an inductive characterization of the set SN גex. We extended the specifi cation already done in Coq for the -calculus by B. Aydemir et al, using nominal logic to build principles of ג -structural induction and recursion. In this way our specification includes the explicit substitution (s[x=t]) in the grammar of the terms. We go foward by de_ning the rewriting systems and the reduction relations for the ג ex and we conclude by formalizing some results for this calculus, as follows: The FC (Full Composition), SIM (Simulation of One Step of β -Reduction) and others that go in the direction of the formalization of the PSN.
metadata.dc.description.unidade: Instituto de Ciências Exatas (IE)
Departamento de Ciência da Computação (IE CIC)
Descripción : Dissertação (mestrado) - Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010.
metadata.dc.description.ppg: Programa de Pós-Graduação em Informática
Aparece en las colecciones: Teses, dissertações e produtos pós-doutorado

Mostrar el registro Dublin Core completo del ítem " class="statisticsLink btn btn-primary" href="/jspui/handle/10482/7685/statistics">



Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.