Well, it’s been quite some time since I posted anything, because this was one busy semester (even without coffee spoons). A lot has been going on here at U. Iowa to keep me from finding time for blogging. One of the biggest things, which might be of interest to some, is the big bump in enrollment which expanded my undergraduate Programming Languages class by 50% from around 60 registered students to 90. This is because it is a required class for majors, and our enrollments are up a lot, as at a lot of other places. The shocker to me was just how much email the class generated. There were 4 programming assignments, 12 short assignments, a midterm and a final. Most of the emails for the class were, I believe (but have not tried to confirm) related to the programming assignments. Since I keep all my email, I can tell you that the course generated around 1,075 emails, of which I personally wrote around 430. For a class that runs 15 weeks (or 105 days), this comes out to be a little over 4 a day on average. Seems like a lot.
Is it worth it? Yes. It is a very fun class to teach. I try to cover some basic informal ideas from Programming Languages from an implementor’s point of view, using a functional programming language. This has been OCaml for me for the past 4-5 years. I did introduce Haskell and Coq, too, at the very end of the class. I am actually toying with the idea of moving to Agda for Spring 2014, since Agda promises to give me the coding elegance of Haskell, in particular definition by recursive equations, as well as verification power as in Coq. Many students, who have learned programming through Java and Python, found programming in OCaml to be a mind-blowing experience. Imagine what it would be like in Agda! Maybe even too mind-blowing? We will see if I am brave enough to try the experiment. I have to learn Agda first, which hopefully we’ll manage this summer.
One example assignment we did was to write a compiler from a high-level language (“rsketch”) similar in spirit to Logo, but using notation for regular expressions, to Processing. This makes a nice connection back to the class, since I learned about Processing from a former student, JJ Meyer. I quite liked these rsketch programs (students had to compete for “audience favorite” for 5 points), as well as many others (f is for forward, r n for rotation by n degrees, cr+ n for increasing the red component of the drawing color by n, l+ n for increasing the length of the segment to draw by n, etc.):
This past week we held a mini-symposium here at U. Iowa. Cody Roux, postdoc’ing with Jeremy Avigad at CMU, and Muhammad Nassar, a doctoral student working with Geoff Sutcliffe at U. Miami, were here for the week. We also had talks from a number of us here, and John Altidor, a doctoral student from U. Mass. Amherst who happened to be in Iowa City for the semester and joined our group for that time. I talked a lot of type theory with Cody, and worked on StarExec in support of TPTP with Muhammad. It was quite productive. I really liked hearing about Cody’s research agenda on the structural theory of PTSs, where he looks to see what operations on PTSs preserve normalization. This was very cool, and Cody had some great technical results and insights about things like why adding individual quantification to F_omega to formulate the Calculus of Constructions does not increase the proof-theoretic strength of the system. This is work in progress, it seems — hopefully a paper will appear soon.
So, that’s a short update. I have something more substantial to blog about soon, namely dualized type theory, which we — Harley Eades III, Ryan McCleeary, and I — are hard at work developing. But that will have to wait till later in the week or next week.