01
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.
↗