Recently I started reading the book Types and Programming Languages. And I found it interesting to proof the lemmas in the book using Coq.

Continue reading →