I hadn't been aware of Tarau's work:<p><a href="http://www.cse.unt.edu/~tarau/" rel="nofollow">http://www.cse.unt.edu/~tarau/</a><p>The real treasure looks like being his theory of isomorphisms:<p><a href="http://logic.csci.unt.edu/tarau/research/2010/ISO.pdf" rel="nofollow">http://logic.csci.unt.edu/tarau/research/2010/ISO.pdf</a><p>I haven't read it all yet, but it reminds me a bit of the
isomorphic kernel described here:<p><a href="http://www.informatik.uni-marburg.de/~rendel/unparse/rendel10invertible.pdf" rel="nofollow">http://www.informatik.uni-marburg.de/~rendel/unparse/rendel1...</a><p>Discusion on LtU here:<p><a href="http://lambda-the-ultimate.org/node/4191" rel="nofollow">http://lambda-the-ultimate.org/node/4191</a><p>Sometimes wading through the noise on HN is worth it when gems like this turn up.<p>Mik