Abstract
A theorem-proving system derived from Higher Order Logic (HOL) is described. The system is designed to support the verification of code written in its own implementation language (SML/NJ), and to allow code which is proven to preserve equality of hol_terms to be used to extend the system. The extension is shown to be theoretically conservative, and the implementation to be reliable. It is hoped that significant efficiency gains can be realized employing this technique (Computational Reflection).
Cite
CITATION STYLE
Woodcock, M. E. (1999). The wHOLe system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1641, pp. 359–366). Springer Verlag. https://doi.org/10.1007/3-540-48257-1_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
