Prof. Aaron Stump has just published a book entitled Verified Functional Programming in Agda, with the new ACM Books series from the ACM. In this book, Prof. Stump provides an introduction to the advanced programming language Agda, suitable for undergraduate Computer Science majors. In Agda, one writes pure functional programs, as in the more widely known language Haskell, but in addition, Agda gives programmers the power to prove properties about their programs using mathematical induction. Furthermore, Agda has a very advanced type system that enables some programming idioms that are not possible in similar typed languages. Verified Functional Programming in Agda is the first book about programming in Agda, and it is the ninth volume published in the ACM Books series.

More information at publisher's website.

An endorsement of Stump's book can be found in the Communications of the ACM June 2017 edition.