Verificação de propriedades do cálculo גex em Coq

AUTOR(ES)

Washington Luís Ribeiro de Carvalho Segundo

DATA DE PUBLICAÇÃO

2010

RESUMO

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.

ASSUNTO(S)

formal verification verificação formal cálculos de substituições explícitas ex outros explicit substitutions calculi ג ex-calculus cálculo ג

Documentos Relacionados

• Uma formalização da composicionalidade do cálculo lambda-ex em Coq
• Custo unitário básico (CUB) : verificação e validação do modelo de cálculo
• Um método geral de cálculo para verificação de estruturas de concreto em situação de incêndio
• Aplicação da equação de Poisson-Boltzmann ao cálculo de propriedades dependentes do pH em proteínas
• Avaliação do metodo semi-empirico HAM-3 no calculo de propriedades moleculares