Kind (an efficient proof and programming language) retargeted to HVM (a garbage-collection-free virtual machine based on interaction nets).