Coq My excursions with the Coq Theorem prover cpdt-ex has my (ongoing) solutions for Adam Chlipala's Certified Programming with Dependent Types.