Matita is a graphical interactive theorem prover based on the calculus of (co)inductive constructions.