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: isabelle-hol

Lawrence Paulson and Isabelle: A Generic Theorem Prover for Many Logics

Lawrence Paulson designed Isabelle as a generic proof assistant in which different object logics could be represented inside one trusted framework, later developing Isabelle/HOL into a major environment for formal mathematics and verification.

↗

seL4 and the Machine-Checked Proof of a General-Purpose Microkernel

seL4 connected a high-performance microkernel implementation to a formal specification with machine-checked proofs, pushing software verification into the privileged operating-system core.

↗