Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Springer LNCS 1166, pp. 265-269, 1996.
Many theorem provers, model checkers and other hardware verification tools are tied to a particular set of facilities and a particular style of interaction. However HOL Light offers a wide range of proof tools and proof styles to suit the needs of various applications. For work in high-level mathematical theories, one can use a more `declarative' textbook-like style of proof (inspired by Trybulec's Mizar system). For larger but more routine and mechanical applications, HOL Light includes more `procedural' automated tools for simplifying complicated expressions, proving large tautologies etc. We believe this unusual range makes HOL Light a particularly promising vehicle for floating point verification, which involves a mix of abstract mathematics and concrete low-level reasoning. We will aim to give a brief tutorial introduction to the system, illustrating some of its features by way of such floating point verification examples. In this paper we explain the system and its possible applications in a little more detail.
@INPROCEEDINGS{harrison-demo, title = "{HOL} Light: A Tutorial Introduction", author = "John Harrison", booktitle = "Proceedings of the First International Conference on Formal Methods in Computer-Aided Design ({FMCAD}'96)", editor = "Mandayam Srivas and Albert Camilleri", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", volume = 1166, year = 1996, pages = "265--269"}