Aaron Stump: Verified Functional Programming in Agda
ACM, 2016, 283 pp, ISBN: 978-1-970001-27-3. https://dl.acm.org/doi/book/10.1145/2841316.
This book is a practical introduction to the dependently-typed functional programming language Agda. The main focus of the book is verified programming, where properties are expressed through a very expressive type system, based on dependent types. In this setting, code that type-checks is also an actual proof of the stated property.