THE LIVING ARCHIVE

From punched cards to autonomous collaborators: the ideas, people, languages and systems that taught machines to follow—and increasingly interpret—human intent.

PAST / PRESENT / NEXT

Collection

Tag: higher-order-logic

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.

↗