01
Mike Gordon and HOL: Higher-Order Logic Becomes a Verification Workbench
Mike Gordon’s HOL system adapted the LCF trusted-kernel style to higher-order logic and showed that a general logical formalism could be used for practical hardware specification and mechanized verification.
↗