Examples are modulus type theory, and here the proof checkers which have been built directly onto this constructive type theory are NUPRL built in the USA and ALF in Sweden, then COQ and LEGO systems which correspond to encoding of these constructive type theories. Higher order logic, they proof general framework is called Isabelle. The Edinburgh logical framework is another framework logical framework called Elf.
A lot of people since the late seventies have worked in this area. And h3ere I have mentioned a few. There are, as you see, people from all over the world.
As I said there is a case for systems systems. This is essentially the Brown's principle. If we are going to use these tools to verify proofs, the tools themselves may be faulty. How are we going to certify the tool itself, unless the tool is simple, we are not certain that it is reliable.
Therefore we have to carry out somehow by hand the verification of our verifier. So, that's why there is a case for weak systems. This is called the Bruijn's principle.