Formal Development for a Node Replication Calculus with Abstract Machine Extraction for a Lazy Strategy

• Felipe A. Costa UFG
• Daniel Ventura UFG

DOI: https://doi.org/10.5753/wbl.2025.8267

Resumo

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 was 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 (currently known as Rocq), following an approach based on refocusing, allowing the automatic extraction of the corresponding abstract machine.

Referências

Ariola, Z. M. and Felleisen, M. (1997). The call-by-need lambda calculus. J. Funct. Program., 7(3):265–301.

Balabonski, T., Barenbaum, P., Bonelli, E., and Kesner, D. (2017). Foundations of strong call by need. Proc. ACM Program. Lang., 1(ICFP):20:1–20:29.

Barendregt, H. P. (1985). The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland.

Biernacka, M. and Charatonik, W. (2019). Deriving an abstract machine for strong call by need. In FSCD, volume 131 of LIPIcs, pages 8:1–8:20. Schloss Dagstuhl - LZI.

Diehl, S., Hartel, P. H., and Sestoft, P. (2000). Abstract machines for programming language implementation. Future Gener. Comput. Syst., 16(7):739–751.

Gundersen, T., Heijltjes, W., and Parigot, M. (2013). Atomic lambda calculus: A typed lambda-calculus with explicit sharing. In LICS, pages 311–320. IEEE CS.

Hannan, J. and Miller, D. (1992). From operational semantics for abstract machines. Math. Struct. Comput. Sci., 2(4):415–459.

Jones, S. L. P. (1992). Implementing lazy functional languages on stock hardware: The spineless tagless g-machine. J. Funct. Program., 2(2):127–202.

Kesner, D. (2009). A theory of explicit substitutions with safe and full composition. Log. Methods Comput. Sci., 5(3).

Kesner, D., Peyrot, L., and Ventura, D. (2024). Node replication: Theory and practice. Log. Methods Comput. Sci., 20(1).

Lamping, J. (1990). An algorithm for optimal lambda calculus reduction. In POPL, pages 16–30. ACM Press.