HOL is a general theorem proving system developed at the University of Cambridge. Developed as a mechanization of a higher-order logic, HOL is now being used in a variety of applications ranging from hardware design verification to reasoning about communication protocols. The purpose of this workshop is to bring together the HOL user community to exchange ideas about the future directions for HOL. The workshop topics include: progress in integrating HOL into more traditional design and development environments; scrutiny of HOL from logicians expert in higher-order logics; application of HOL as a formal methods tool in verification.
