Also, Thierry Coquand, who is behind CoC, and is also one of the developers of the software that became Coq.