Verified Functional Programming in Agda |
|
| Author:
| Stump, Aaron |
| Series title: | ACM Bks. |
| ISBN: | 978-1-970001-24-2 |
| Publication Date: | Feb 2016 |
| Publisher: | Morgan & Claypool Publishers
|
| Book Format: | Paperback |
| List Price: | USD $79.95USD $79.95 |
Book Description:
|
Provides a systematic exposition of external and internal verification in Agda, suitable for undergraduate students of computer science. The book begins with an introduction to functional programming through familiar examples like booleans, natural numbers, and lists, and techniques for external verification. More advanced material on type-level computation, explicit reasoning about termination, and normalization by evaluation is also included.
Provides a systematic exposition of external and internal verification in Agda, suitable for undergraduate students of computer science. The book begins with an introduction to functional programming through familiar examples like booleans, natural numbers, and lists, and techniques for external verification. More advanced material on type-level computation, explicit reasoning about termination, and normalization by evaluation is also included.