Benjamin Pierce has a course on the mathematical theory of programming languages, using the Coq Proof Assistant: http://www.cis.upenn.edu/~bcpierce/sf/toc.html

Benjamin Pierce has a course on the mathematical theory of programming languages, using the Coq Proof Assistant: http://www.cis.upenn.edu/~bcpierce/sf/toc.html http://www.cis.upenn.edu/~bcpierce/sf/toc.html Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/