James Cheney, Christian Urban: Mechanizing the Metatheory of mini-XQuery. CPP 2011: 280-295