[Agda] release schedule, coding suggestions, book

Aaron Stump aaron-stump at uiowa.edu
Wed Nov 5 18:56:34 CET 2014


Hello, Agda community.  I am teaching a class on functional programming 
Spring 2015 using Agda (I did this Spring 2014, too).  I have a couple 
of questions you can probably help me with:

1. Are there any planned new releases of Agda between now and, say, 
mid-February?  I want to start the class off with the latest version of 
Agda, but since we will be bundling Windows MSI files for Agda, I need 
to plan ahead for what that release might be.  In general, is a planned 
release schedule posted somewhere on the Wiki?  I did not notice it in a 
quick inspection.

2. I am planning on turning the class into a lemma-proving factory. I 
have always dreamed of doing this, and the results were pretty good 
Spring '14.  Since we only care if lemmas type-check (unless time to 
type check becomes an issue), student solutions can be incorporated into 
a library without further scrutiny.  Do you have suggestions or requests 
for reasonably basic FP algorithms or building blocks we could prove 
properties of?  I will likely try to get inspiration from the Haskell 
Prelude, just as an example, but I thought I would ask.  I will be 
including whatever we develop as part of the "Iowa Agda Library", whose 
current version is available here:

https://svn.divms.uiowa.edu/repos/clc/projects/agda/lib

Username and password are both "guest" (without the quotes) if prompted.

3. I am also writing a book called "Verified Functional Programming in 
Agda".  I have a good bit more to go, but hope to be completing a draft 
by the end of Spring '15.  I am currently talking with publishers, and 
could publish with a company called Cognella, which focuses on niche 
textbooks.  I am curious if others might possibly be interested in using 
such a book for class.  The more copies I can assure the publisher would 
be sold, the lower the price I can negotiate.  The current draft -- 
rather spotty currently -- is here

https://svn.divms.uiowa.edu/repos/clc/projects/agda/book

Again, username and password are guest if you are asked.  The focus is 
on basic verification methods for pure functional programs, rather than 
advanced Agda (which I do not know much of anyway).

Thanks,
Aaron


More information about the Agda mailing list