I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in a fashion of "Token-Passing Nets: Call-by-Need for Free" by François-Régis Sinot. Implementations of optimal reduction that I am aware of either assume a specific strategy for the interaction net reduction, or involve non-pure graph reductions rather than just interaction rules.

The reason why I am interested in such implementation is that I already have a compiler for interaction nets which is based on interaction calculus, but is agnostic to any notion of interface, thus unable to follow any strategy while reducing a configuration simply represented as a queue of active pairs.

I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis Sinot. Implementations of optimal reduction that I am aware of either assume a specific strategy for the interaction net reduction, or involve non-pure graph reductions rather than just interaction rules.

The reason why I am interested in such implementation is that I already have a compiler for interaction nets which is based on interaction calculus, but is agnostic to any notion of interface, thus unable to follow any strategy while reducing a configuration simply represented as a queue of active pairs.

I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in a fashion of "Token-Passing Nets: Call-by-Need for Free" by François-Régis Sinot. Implementations of optimal reduction that I am aware of either assume a specific strategy for the interaction net reduction, or involve non-pure graph reductions rather than just interaction rules.

The reason why I am interested in such implementation is that I already have an compiler for interaction nets which is based on interaction calculus, but is agnostic to any notion of interface, thus unable to follow any strategy while reducing a configuration simply represented as a queue of active pairs.

I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in a fashion of "Token-Passing Nets: Call-by-Need for Free" by François-Régis Sinot. Implementations of optimal reduction that I am aware of either assume a specific strategy for the interaction net reduction, or involve non-pure graph reductions rather than just interaction rules.

The reason why I am interested in such implementation is that I already have a compiler for interaction nets which is based on interaction calculus, but is agnostic to any notion of interface, thus unable to follow any strategy while reducing a configuration simply represented as a queue of active pairs.