My Coq proofs for the TAPL book. Work in progress, come back in a few years.

  ------
 | Coq! |
  --  --
    \/   v
     \ -<O___,,
          \VV/
           //

Some quick notes for the future me:

To generate CoqMakefile I've used:

$ coq_makefile -f _CoqProject -o CoqMakefile

See the docs.

I recommend using pLam to play around with pure λ-calculus.