HOL with Definitions: Semantics, Soundness, and a Verified Implementation.

Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens

Browse the full ITP paper archive.