Title: Certified Programming with Dependent Types
Subjects: Automatic theorem proving, Computer programming, Computer programs, Coq (Electronic resource)