About this room
- Dependent type theory: Coq / Rocq, Lean, Agda, Nuprl, F*, Idris.
- Higher-order logic: Isabelle/HOL, HOL4, HOL Light, PVS.
- Set-theoretic or foundational systems: Mizar, Metamath.
- Logical frameworks: Twelf, Beluga, Dedukti.
- Program-verification systems: Dafny, Why3, VeriFast, VST, Frama-C.
- Mostly automated provers: ACL2, Z3, CVC5, Vampire, E, SPASS.
