The Free On-line Dictionary of Computing (19 January 2023):

HOL-88

   An implementation of HOL built on ML by Mike Gordon
   .