I would add, re: Shen -- it's sequent calculus and unique type system (type system itself is Turing complete) give you a lot of flexibility here.

Shen is one of those projects i've always wanted to dig into a bit but have never found the time sadly.