2025-06-052025-06-052024-12-13COSTA, 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.http://repositorio.bc.ufg.br//handle/ri/27710Node-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.engAcesso Abertohttp://creativecommons.org/licenses/by-nc-nd/4.0/Máquina abstrataReplicação nó-a-nóAvaliação preguiçosaRefocusingNode-replicationFull-lazinessAbstract machineTrabalho de conclusão de curso de graduação (TCCG)