Ebook Certified programming with dependent types: Part 2 - Adam Chlipala

Continued part 1, part 2 of ebook "Certified programming with dependent types" provides readers with contents including: proof engineering; the big picture; proof search by logic programming; proof search in Ltac; proof by reflection; proving in the large; a taste of reasoning about programming language syntax; parametric higher-order abstract syntax; building a reification tactic that recurses under binders;...