The Free On-line Dictionary of Computing (30 December 2018):

HOL-88

   An implementation of HOL built on ML by Mike Gordon
   .