[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