Indeed I have, though I have some reservations about its focus on interaction nets (or rather, its marketing). I ended up making a CUDA-based, data-parallel ST

Indeed I have, though I have some reservations about its focus on interaction nets (or rather, its marketing). I ended up making a CUDA-based, data-parallel STLC typechecker (Hindley-Milner)... I want to formally prove its correctness first, but maybe a blog post would be okay either way.