Variants of intuitionistic type theory underlie several widely used proof assistants, including NuPRL, Coq, and Agda. These proof assistants are computer systems that have been used for formalizing large and complex proofs of mathematical theorems, such as the Four Colour Theorem in graph theory and the Feit-Thompson Theorem in finite group theory. They have also been used to prove the correctness of a realistic C compiler (Leroy 2009) and other  computer software.