The interactive textbook Software Foundations, by Benjamin C. Pierce et al., introduces logic, the Coq proof assistant, and applications to the theory of programming languages. It has been used at universities around the world (and for independent study) since 2008.
For DeepSpec, the textbook has been rewritten and expanded. In Spring 2017 we will be dividing the material on logic and programming languages into two volumes, 1. Logical Foundations and 2. Programming Language Foundations. A new volume, 3. Verified Functional Algorithms by Andrew W. Appel, is for those who want to teach (or learn) the verification of programs and not only programming languages. Volume 3 depends on material only from Volume 1. An instructor can teach Volume 1 in half a semester, then choose material from Volumes 2 and 3 for the second half of the semester.
Volume 4. Separation Logic by Arthur Charguéraud is in preparation. Volume 5. Systems Verification is planned for the future.