Coq is an interactive theorem prover made for formalizing
mathematical theories and algorithms using type theory. I am fond of
using it to prove everything that is shown to me and I don't
understand at first. So here's a list of Coq stuff I use to prove
things and some developments.
A formalization of simply-typed lambda calculus and its proof of
normalization using a kripke model. Includes a proof that peirce's
law is not derivable using models and the syntactic characterization
of normal forms. This is joint work with Thorsten Altenkirch.
Algebra of Programming Using Dependent Types in Mathematics of Program Construction. Shin-Cheng Mu, Hsiang-Shang Ko & Patrik Jansson. Philippe Audebaud and Christine Paulin-Mohring (Eds). Volume 5133 of Lecture Notes in Computer Science. Berlin Heidelberg: Springer-Verlag, July 2008, pp.268-283.