This is an old revision of the document!
XCend is based on a full formalization in Isabelle/HOL.
The full theory (as HTML and PDF) can be found here.