A token-passing net implementation of optimal reduction with embedded read-back
Anton Salikhmetov

TL;DR
This paper presents a novel token-passing net implementation of optimal reduction for untyped lambda calculus, enabling strategy-independent normalization and integrated read-back within interaction nets.
Contribution
It introduces a token-passing net approach for optimal reduction with embedded read-back, enhancing flexibility and formalism integration.
Findings
Achieves normal form regardless of reduction strategy
Integrates read-back mechanism within interaction nets
Demonstrates effectiveness for pure untyped lambda calculus
Abstract
In this paper, we introduce a new interaction net implementation of optimal reduction for pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of interaction net reduction strategy using the approach of so-called token-passing nets. Another new feature is the read-back mechanism also implemented without leaving the formalism of interaction nets.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
