Lines Matching defs:HOL
6 \title[Deep Embeeding of Separation Logic]{A Deep Embedding of a \\Decidable Fragment of Separation Logic in HOL}
11 \newcommand{\HOL}{{\sf HOL}}
97 in \HOL
98 \item a decision procedure for entailments has been implemented in \HOL
102 \item it may be extended to a \HOL\ implementation of \smallfoot
472 \section{HOL embedding}
476 \frametitle{HOL embedding}
478 \item deep embedding in HOL is straight forward except for trees
487 \frametitle{HOL embedding II}
554 \frametitle{example HOL}
579 \frametitle{example HOL II}
600 \item all inferences used by \smallfoot\ have been verified using HOL
607 \item add symbolic execution to build a \smallfoot\ implementation in HOL