<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi, Aaron.<div class=""><br class=""></div><div class="">Thanks for sharing and congrats!</div><div class=""><br class=""></div><div class="">Best,</div><div class="">Harley</div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Feb 29, 2016, at 3:46 PM, Aaron Stump <<a href="mailto:aaron-stump@uiowa.edu" class="">aaron-stump@uiowa.edu</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="content-type" content="text/html; charset=utf-8" class="">
<div text="#000000" bgcolor="#FFFFFF" class="">
Dear Agda community,<br class="">
<br class="">
I am writing to let you know about a textbook I have written based
on Agda, called "Verified Functional Programming in Agda" (VFPiA).
This has been published now as part of the ACM Books series from
ACM. The book is intended as an introduction for undergraduates who
do not have a background in Agda, or type theory, or even functional
programming. (Note that the book is not intended to be a reference
on advanced features of Agda; that would be a great book for others
on this list to write!) The goal of VFPiA is an introduction, for
beginners, to ideas in applied type theory using Agda. I'm
attaching the TOC, to give you an idea of what is covered. I have
been teaching undergrads at The University of Iowa from this for the
past two years, with encouraging results. It would also be suitable
for industrial practitioners or others interested in learning more
about using Agda for verified programming.<br class="">
<br class="">
You can find VFPiA on Amazon and other online booksellers. Also,
the publisher, Morgan and Claypool, is offering the Agda list the
friends and colleagues discount of 15% for the book. Just use the
code "authorcoll" (without the quotes) when shopping at Morgan and
Claypool directly:<br class="">
<br class="">
<span style="" class=""><a href="http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=908" class=""></a><a class="moz-txt-link-freetext" href="http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=908">http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=908</a></span><br class="">
<br class="">
The book cover is below, for your interest.<br class="">
<br class="">
My hope is that the book will help promote Agda!<br class="">
<br class="">
Best wishes,<br class="">
Aaron<br class="">
<br class="">
<span id="cid:part2.04050204.03070403@uiowa.edu"><cover.jpg></span><br class="">
</div>
<span id="cid:D1B229A6-BF4B-4FD2-A36E-8E58B241A0B1@aug.edu"><toc.pdf></span>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>