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) is available here:
| Version || Description || Document
| ITP || Published at ITP 2012 in Princeton. || paper
| PhD || The accompanying theory of the PhD thesis. || in revision