If you haven't done so already, you might want to look at interaction nets and HVM. Although HVM does not (yet!) support full lambda calculus. I'm currently ex

If you haven't done so already, you might want to look at interaction nets and HVM. Although HVM does not (yet!) support full lambda calculus. I'm currently exploring another approach to a massively parallel reducer for pure lambda calculus. Efficient sharing of lambda graphs is one of the main problems for me.