Prof. Aaron Stump is celebrating a double thousand: a thousand downloads of his book "Verified Functional Programming in Agda" and a thousand plays of his new podcast "The Iowa Type Theory Commute." Says Stump, "My goal with both these works is to try to bring research ideas in advanced functional programming and constructive logic to a broader audience than just professional researchers. I am thrilled to reach a thousand accesses, right around the same time, for both of these."

 

Stump's Agda book, published by ACM Books, is the first textbook on Agda, a language which combines functional programming and constructive mathematical reasoning.

 

The podcast, recorded on his daily short commute to The University of Iowa, has an intended audience of programmers and enthusiasts interested in learning more about advanced functional programming and computer-checked proofs. Laughs Stump, "the podcast is also intended to double as not-so-subtle advertising for the great quality of life we enjoy here in Iowa. Many of my listeners probably have to queue up three or four of these episodes on their big-city commutes."