[leshow]

C++ metaprogramming might not be pretty, but it's extremely expressive, I'd be surprised if it didn't have some kind of type theoretic background.