Measuring out your life with…

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.):

  ( f r 20 cr+ 4 w+ 1 l+ 1 cg+ 5 cb+ 3 f r 255 ) * 1200

and

  ( h ( f r 30 l+ 1 cb+ 1 ) * 80 l- 80 r 5 cg+ 30 ) * 120

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.

Midwest Verification Days 2012

Last week, a bunch of us from U. Iowa (8 in total, in two rental cars) drove down to Kansas U. for Midwest Verification Days (MVD), hosted by Perry Alexander and Andy Gill, and very efficiently supported by the wonderful staff there at the Kansas Information and Telecommunication Technology Center (ITTC).  As has become the norm for MVD, it was a lively meeting, with around 60 participants, and a very high level of talks.  Most of the talks were from graduate students, though undergraduate Angello Astorga (who worked with me this past summer) came down from Ohio State to talk about his summer work, and there were also great industry talks by Lee Pike of Galois and Ray Richards and David Hardin of Rockwell Collins.  You can see the full schedule on the MVD ’12 page.  Galois and Rockwell were both in recruiting mode, as well as telling us about the amazingly cool applications of formal methods that their companies are pursuing.  I would love to see MVD become a recruiting event, as well as a research event.  We are clearly on our way with the presence of these two important formal-methods teams.

As I said, the student talks were really great.  I personally always love hearing the talks from the U. Colorado Boulder group.  They are always doing some cutting-edge applications of static analysis or formal methods to current development problems.  For example, Arlen Cox and Devin Coughlin were talking about static analysis for Javascript — very relevant for web programming, of course, and posing nasty analysis problems as the language and idioms for it are very dynamic (e.g., method calls by reflection) and hard to deal with statically.  Sam Blackshear  was talking about live-leak detection, which I always thought was an intriguing problem.  Really, all the talks were great, and I don’t have time to tell you about all of them.  So I have to just mention a couple more.  I really liked a talk by Caleb Eggensperger of U. Oklahoma on ProofPad, a nice graphical interface for ACL2.  The talk by Dongjiang You of U. Minnesota Software Engineering Center on Observable MC/DC (a code coverage method I’d heard his advisor Mike Whalen talk about before), was also very interesting to me: the idea I took away (and I’m not too familiar with code-coverage techniques) was that we could execute a piece of code with concrete inputs, while still tracking which internal variables contribute to the output.  This could help us see which internal parts of a system are being exercised by a concrete test case.  That’s a cool mix of static and dynamic semantics (since we have a dynamic execution that tracks some static information, namely which variables contributed to a concrete value), which I had not considered before.

Anyway, it was a really fun event, and I’m very pleased that MVD is alive and well, following what is now the 4th edition (MVD ’09 and ’10 were the first ones, at Iowa; and then MVD ’11 was at Minnesota).  MVD ’13 will be at U. Illinois Chicago, hosted by Lenore Zuck, who was also there at MVD ’12, so that is going to be very exciting as well.  Our definition of the Midwest is pretty broad, and Midwesterners are welcoming people by nature: so swing by for the  next one if you can.

Recent travel

It has been the busiest semester on record for me here at The University of Iowa, Computer Science department, due to a lot of group activity. Just one aspect of this has been travel for people I work with, from the summer up until now:

• I presented our paper “Type Preservation as a Confluence Problem” at RTA in Novi Sad, Serbia.
• Duckki Oe presented our paper “Combining a Logical Framework with an RUP Checker for SMT Proofs” at the SMT workshop, in Snow Bird, Utah.
• Frank (Peng) Fu presented our paper with Jeff Vaughan “A Framework for Internalizing Relations into Type Theory” at the PSATTT workshop at CADE, in Wrcolaw, Poland (which necessitated an elaborate visa-renewal trip for Frank to China).
• Duckki Oe also gave a talk at the DTP (Dependently Typed Programming) workshop in Nijmegen, The Netherlands, on his versat verified SAT solver tool, which is fully proved (all lemmas done, showing that if the solver says UNSAT, there is guaranteed to exist a resolution proof of the empty clause from the input clauses, although this proof is not actually created at runtime) and fully operational at this point.
• Harley Eades gave a talk on his work on hereditary substitution for variants of predicative System F, at the well-known TYPES meeting, in Bergen, Norway.  You can read about his trip on his new blog, Metatheorem.
• Garrin Kimmell gave a talk at a Shonan meeting (in Japan) on dependently typed programming on call-by-value equational reasoning and general recursion in our Sep3 language, a design being developed in the context of the Trellys project, which I’ve blogged about before.
• And of course, we all went up to Midwest Verification Day in Minneapolis, Minnesota.  This was a great event, where we got to see some of our friends working on verification-related topics, from other schools in the Midwest.  I had interesting conversations with Grigore Rosu and Eric Van Wyk, and was really pleased to meet David Pichardie for the first time in person.  He and two students drove over from Purdue, where they are visiting Jan Vitek to collaborate on compiling Java Byte Code to CompCert C (CompCert is a project developing a verified optimizing C compiler in Coq, led by Xavier Leroy).

So, it has been busy with travel for us (and that doesn’t count trips like to summer schools, or by other members of the group who work primarily with Cesare Tinelli).  We definitely have a full semester under way as well, but I will write more about that later (you can get a small taste at the blog I am keeping for my seminar for first-year undergrads, on Hidden Meanings).

PLPV 2012 PC Chairs Set

Just a quick post: the PC chairs for PLPV 2012, to be collocated with POPL 2012 in Philadelpha, PA, have been set now.  They are Koen Claessen and Nikhil Swamy.  It is really great for the workshop to have such exciting PC leadership for this next edition.  So get ready for a great PLPV in January!

Report from RTA ’11

RTA 2011 was held in Novi Sad, Serbia, the last week of May, as part of the RDP 2011 federated conference, which brings together RTA and TLCA every two years.   I was not able to attend any of TLCA ’11, though the program looked quite exciting.  RTA was really great, though.  Silvia Ghilezan, who served as the conference chair for both conferences, did an outstanding job in ensuring that the conference logistics ran smoothly and pleasantly, including excursions in the local area.  For me, this was quite interesting, since my family on my wife’s side is Bulgarian, and there are a lot of cultural and linguistic similarities between the two countries (although no doubt people with longer experience would tell me there are many differences, too).  I was able, occasionally, to get somewhere using my baby Bulgarian, although the shuttle driver from the airport warned me that the languages only share about 30% of their words.

Anyhow, back to RTA.  The technical program was quite fascinating for me.  The invited talk by Sophie Tison surveyed results at the intersection of tree-automata theory and term rewriting, including so-called “preservation of recognizability”.  The idea is to study what classes of term-rewriting systems preserve recognizability of a set of terms by a tree-automaton.  That is, if a set T of terms is recognizable by a tree automaton, under what conditions (on the term-rewriting system) is the set of descendants (or alternatively, ancestors) of terms in T is recognizable by a tree automaton.  There is apparently a line of literature on this problem, which Sophie Tison surveyed in her talk, along with several other interesting variations on tree automata (particularly ones with equality and disequality constraints).  Tree automata are studied in the nice book, available online, Tree Automata Techniques and Applications (“TATA”), of which Sophie Tison is a co-author. This would make a nice topic for a CLC seminar…

I really enjoyed many talks in the program, and this post will go on forever if I transcribe my 10 pages of notes.  Let me just hit a couple exciting highlights.  Fer-Jan de Vries gave a very interesting talk related to confluence of infinitary lambda calculus.  The best thing for me about this talk was that it included a reminder of the basic fact (unknown to me before this) that infinitary lambda calculus is not convergent, under at least some notion of infinitary reduction (there are several, and they involve defining a notion of limit of an infinite reduction sequence).  A counterexample is the term , defined as follows:

• 
• 
• 

We have reducing (finitarily, and also in the limit, apparently) to .  But we also have

The limit of this sequence is an infinitary term .  And that term is not joinable with .  Pretty weird!  Just another example of how infinity tends to defy our finitary intuitions.

There was an amazing tool talk about Anagopos, a visualization tool for lambda calculus and term rewriting reductions.  This tool can draw pretty mind-blowingly cool graphs representing reductions of lambda-calculus terms, and related things.  The two Danish (I believe) Master’s students who presented this did a fine job, both with the tool and the talk.

Ok, I guess I am transcribing my notes a bit.  There was a lot of very interesting material.  René Thiemann had some very interesting things to say about the Termination Competition.  One example: in every competition since 2004, including the 2011 edition, there have been tools producing wrong answers.   Now, the good news is that the Termination Competition has a certified division, where tools produce proofs which are then checked by certifiers based on proof assistants like Coq.  This means they get a rather high degree of confidence that results are correct, at least for this division.  René noted later that the CETA certifier has a fully verified parser — this is an interesting point, since I have read not that long ago that tools like the Compcert verified C (subset) compiler lack this, and it is actually a source of bugs for Compcert (where the rest of the compiler, which has been proven sound in Coq, is bug free).  This was discussed in the fantastic paper, which I saw referenced on Lambda the Ultimate, by John Regehr et al. entitled “Finding and Understanding Bugs in C Compilers”.  Since I saw this through LtU, I did not want to post about it independently, but man that is a great paper.  Everyone interested in compilers and verification should definitely read it.

A few quick other things, as I need to wrap this up.  I had many great conversations with very interesting people, including Georg Moser, a proof-theorist who is working now in automated complexity analysis for term-rewriting systems.  He had a very impressive paper showing that the dependency-pair framework for showing termination of term-rewriting systems gives essentially the mutliply recursive functions, which are (apparently) those derivable using only primitive recursions at type of order 1 (I always get confused about whether orders of types start at 0 or 1 — this is the type ).  I also had a very nice conversation with Nao Hirokawa, whose clever ideas and excellent research agenda very much impressed me.  Nao is also a co-organizer of the recently announced Confluence Competition (CoCo), which will run for the first time in 2012.  I am talking with Nao about his possibly visiting me at The University of Iowa this fall sometime, which would be fun and really great for our group.  Ashish Tiwari gave a great invited talk about applications of term-rewriting to systems biology, and other topics.  This was also a really impressive talk, as Ashish summarized a bunch of very strong work with interesting applications.  Stephanie Weirich, with whom I collaborate, along with Tim Sheard, on the Trellys project, gave the sole shared invited talk between RTA and TLCA — quite an honor.  She gave a great talk, which sparked a lot of interesting conversations with people like Andreas Abel, Thorsten Altenkirch, and Peter Dybjer, all of whom I got to speak with later that day.

In the end, I emerged convinced that RTA is a gem of a conference, with a pleasant and very serious core community, which is also quite welcoming to relative newcomers (such as myself).  The acceptance rate is higher than they’d like (around 55% for this edition), which is not necessarily a bad thing if you are an aspiring author.  The next edition, RTA ’12, will be in Nagoya, Japan.  I also heard from several people that they were interested in possibly coming to the US for a later edition.  I am seriously considering proposing Iowa City, Iowa, for the next available RTA, which looks to be RTA 2015 (as 2013 is in Eindhoven, and 2014 will be with FLoC).  That would be an RDP year, so if I did propose this, and the proposal were accepted, that would bring RTA and TLCA to The University of Iowa, which would be super cool for us, and probably also for many researchers interested in types (for TLCA) and rewriting in North America.