[Agda] announcing Verified Functional Programming in Agda

[Jon Sterling]

Hi Aaron,

This looks fantastic, thanks for sharing!

best,
jon


On Mon, Feb 29, 2016, at 01:15 PM, Harley Eades III wrote:
> Hi, Aaron.
> 
> Thanks for sharing and congrats!
> 
> Best,
> Harley
> 
> > On Feb 29, 2016, at 3:46 PM, Aaron Stump <aaron-stump at uiowa.edu> wrote:
> > 
> > Dear Agda community,
> > 
> > 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.
> > 
> > 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:
> > 
> >  <http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=908>http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=908 <http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?products_id=908>
> > 
> > The book cover is below, for your interest.
> > 
> > My hope is that the book will help promote Agda!
> > 
> > Best wishes,
> > Aaron
> > 
> > <cover.jpg>
> > <toc.pdf>_______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda