dc.contributorMoura, Flávio Leonardo Cavalcanti de
dc.creatorBarros, Flávio José Ferro
dc.date2011-01-26T00:28:37Z
dc.date2011-01-26T00:28:37Z
dc.date2011-01-26T00:28:37Z
dc.date2010-07-19
dc.date.accessioned2017-03-07T12:24:43Z
dc.date.available2017-03-07T12:24:43Z
dc.identifierBARROS, Flávio José Ferro. Uma formalização da composicionalidade do cálculo lambda-ex em Coq. 2010. vii, 61 f. Dissertação (Mestrado em Informática)-Universidade de Brasília, Brasília, 2010.
dc.identifierhttp://repositorio.unb.br/handle/10482/6601
dc.identifier.urihttp://repositorioslatinoamericanos.uchile.cl/handle/2250/349613
dc.descriptionDissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010.
dc.descriptionApresenta-se uma formalização das propriedades de composicionalidade do Cálculo lambda-ex em Coq. A abordagem utilizada baseia-se na lógica nominal de acordo com o trabalho desenvolvido por [3]. Mais especificamente estendemos a formalização do lambda-cálculo contida neste trabalho de forma a incluir a operação de substituição explícita do cálculo lambda-ex. Nessa abordagem, a alpha-equivalência coincide com a igualdade pré-construída de Coq, e os princípios de recursão e indução sobre classes de lambda-termos possuem tratamento específico. Escolhemos trabalhar com o cálculo lambda-ex por ser atualmente o único cálculo que satisfaz simultaneamente todas as propriedades desejáveis para um cálculo de substituições explícitas. Ele é uma extensão do lambda-x com uma regra de reescrita para composição de substituições dependentes e uma equação para comutação de substituições independentes. O cálculo lambda-ex usa um construtor unário para a substituição explicita, mas tem o mesmo poder de expressividade de cálculos com substituições simultâneas. _________________________________________________________________________________ ABSTRACT
dc.descriptionWe present a formalization of properties of compositionality of the ex-calculus in Coq. The approach is based in the nominal logic as presented in the paper [3]. More precisely, we extended a formalization of the -calculus in such a way that it now includes the explicit substitution operation of the ex-calculus. In this approach, -equivalence of -terms coincides with the Coqt’s built-in equality, and the principles of recursion and induction over classes of -terms are treated in a specific way. We chose to work with the ex-calculus because it is currently the only calculus that simultaneously satisfies all the desirable properties for a calculus of explicit substitutions. It is an extension of the x-calculus with a rewrite rule for composition of dependent substitutions and one equation for independent substitutions. The ex-calculus has a unary constructor for the explicit substitution operation, but have the same expressive power of calculi with simultaneous substitutions.
dc.languagepor
dc.rightsOpen Access
dc.subjectLinguagem de programação (Computadores)
dc.titleUma formalização da composicionalidade do cálculo lambda-ex em Coq
dc.typeTesis


Este ítem pertenece a la siguiente institución