Certified Programming with Dependent Types

A Pragmatic Introduction to the Coq Proof Assistant

by Adam Chlipala