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

Abstract

Node-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.