And there are other proof assistants which are not based on type theory. For instance based on equational of logic we have HOL, Isabelle, and PVS. Let me note at this point that these systems are based on a logic with a very heavy syntax. So, in order to have a powerful logic, here we have to make the syntax more complex. Many times these proof checkers do not satisfy the de Bruijn principle. Then there are other proof assistants based, for instance, on set theory. You may see many of these, and others, at the internet address in the slide.

---