1991 International Workshop on the HOL (Higher Order Logic) Verification System and its Applications--Davis, CA, August 26-28, 1991

HOL是剑桥大学开发的一个一般定理证明系统。作为一种高阶逻辑的机械化发展，HOL现在被用于从硬件设计验证到通信协议推理的各种应用中。本次研讨会的目的是将HOL用户社区聚集在一起，就HOL的未来发展方向交换意见。研讨会的主题包括：将HOL整合到更传统的设计和开发环境中的进展；高阶逻辑专家对HOL的审视HOL作为形式化方法工具在验证中的应用。

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.