Formalização de um cálculo de replicação de nós com extração da máquina abstrata para uma avaliação preguiçosa

Página do item simplificado
dc.contributor.advisor1Ventura, Daniel Lima
dc.contributor.referee1Silvestre, Bruno Oliveira
dc.contributor.referee1Ventura, Daniel Lima
dc.creatorCosta, Felipe Aguiar
dc.date.accessioned2025-06-05T15:28:29Z
dc.date.available2025-06-05T15:28:29Z
dc.date.issued2024-12-13
dc.description.abstractNode-by-node replication is related with the implementation of optimal graph-based reduction for the λ-calculus and its associated substitution mechanism was recently identified as the Curry-Howard interpretation of deep-inference. A lazy (weak) strategy is defined for the node-replication calculus, with full-laziness and an observationally equivalent relation equivalent to the same relation for a (weak) call-by-name strategy. A node-replication calculus with a fully lazy call-by-need reduction strategy is specified in the Coq Proof Assistant, following an approach based on a refocusing procedure, allowing the automatic extraction of the corresponding abstract machine.
dc.description.resumoA replicação nó-a-nó está relacionada às computações ótimas para reduções baseadas em grafos do λ-calculus e recentemente a substituição associada foi identificada como a interpretação Curry-Howard da Lógica com Inferência Profunda. A investigação para o cálculo com replicação de nós estabelece propriedades baseadas em sua semântica operacional, definida por um sistema de regras de redução baseadas em contextos, e em sua semântica denotacional, com um sistema de tipos quantitativo. Uma estratégia de avaliação (fraca) preguiçosa é definida para o cálculo, satisfazendo as propriedades de full-laziness e com uma relação de equivalência observacional equivalente a relação para a estratégia de avaliação (fraca) de chamada-por-nome. Neste trabalho é apresentada uma especificação no assistente de provas Coq de um cálculo com replicação de nós com uma estratégia de chamada-por-necessidade, com uma abordagem baseada em refocusing, permitindo que a máquina abstrata associada seja extraída automaticamente a partir da especificação.
dc.identifier.citationCOSTA, Felipe Aguiar. Formalização de um cálculo de replicação de nós com extração da máquina abstrata para uma avaliação preguiçosa. 2024. 47 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) - Instituto de Informática, Universidade Federal de Goiás, Goiânia, 2024.
dc.identifier.urihttp://repositorio.bc.ufg.br//handle/ri/27710
dc.language.isoeng
dc.publisherUniversidade Federal de Goiás
dc.publisher.countryBrasil
dc.publisher.courseCiência da Computação (RMG)
dc.publisher.departmentInstituto de Informática - INF (RMG)
dc.publisher.initialsUFG
dc.rightsAcesso Aberto
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/
dc.subjectMáquina abstrata
dc.subjectReplicação nó-a-nó
dc.subjectAvaliação preguiçosa
dc.subjectRefocusing
dc.subjectNode-replication
dc.subjectFull-laziness
dc.subjectAbstract machine
dc.titleFormalização de um cálculo de replicação de nós com extração da máquina abstrata para uma avaliação preguiçosa
dc.title.alternativeFormalisation of a node replication calculus with abstract machine extraction for a lazy evaluation
dc.typeTrabalho de conclusão de curso de graduação (TCCG)

Arquivos

Pacote Original

Agora exibindo 1 - 1 de 1
Imagem de Miniatura
Nome:
TCCG - Ciência da Computação - Felipe Aguiar Costa - 2024.pdf
Tamanho:
441.89 KB
Formato:
Adobe Portable Document Format
Baixar

Licença do Pacote

Agora exibindo 1 - 1 de 1
Imagem de Miniatura
Nome:
license.txt
Tamanho:
1.71 KB
Formato:
Item-specific license agreed upon to submission
Descrição:
Baixar

Coleções

INF - Trabalhos de Conclusão de Curso