TAPL isn't Coq-focused. Pierce and his collaborators have another book available online, Software Foundations, which is written as a Coq literate program: http:

TAPL isn't Coq-focused. Pierce and his collaborators have another book available online, Software Foundations, which is written as a Coq literate program: http://www.cis.upenn.edu/~bcpierce/sf/index.html http://www.cis.upenn.edu/~bcpierce/sf/index.html