The impossibility of computationally sound XOR (report, 2010)
Dominique Unruh
[ eprint ]

We give a simple example that there is no symbolic theory for exclusive or (XOR) that is computationally sound.