It consists of two parts: a monograph, which is called Dependent Record Types and Formal Abstract Reasoning: Theory and practice, and my licentiate thesis, which is called A case-study in machine assisted proofs: The Integers form an Integral Domain.
Both are gzipped postcript files.