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: trusted-kernel

Robin Milner, LCF, and the Trusted-Kernel Architecture of Interactive Theorem Proving

LCF made a small trusted proof kernel the foundation of an extensible interactive theorem prover, while its ML metalanguage gave users a programmable way to construct proof tactics without expanding the trusted base.

↗