Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.unb.br/handle/10482/7685
Files in This Item:
File Description SizeFormat 
2010_WashingtnLuisRibeirodeCarvalhoSegundo.pdf516,71 kBAdobe PDFView/Open
Title: Verificação de propriedades do cálculo גex em Coq
Authors: 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
Issue Date: 11-May-2011
Citation: 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.
Abstract: 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.
Description: Dissertação (mestrado) - Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010.
Appears in Collections:CIC - Mestrado em Informática (Dissertações)

Show full item record Recommend this item " class="statisticsLink btn btn-primary" href="/handle/10482/7685/statistics">



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.