This is an old revision of the document!
The full formal definition and the proof of type soundness is available here.
