This past Thursday and Friday (Oct. 10th and 11th), I organized a mini-symposium on Programming Languages here at U. Iowa. I invited doctoral students from Indiana, U. Penn., Portland State, and Northwestern to come down and give talks on their research in PL. Robby Findler from Northwestern also brought his fall PL seminar down — so we had a big group of Racketeers here! Sam Tobin-Hochstadt gave the keynote, which was simultaneously our departmental colloquium. Why did I call this a mini-symposium? Isn’t a “symposium” in the ACM taxonomy just a meeting that is between the size of a workshop and a conference? I was thinking of Plato’s symposium here, where the emphasis is on lively discourse in pursuit of truth (about love, in Plato’s case, and involving quite a bit of drinking — while our focus was more technical, we did go for local beer). So we had 45 minutes blocked out for each talk, and lots of breaks and long lunches. I was really happy with the results, as we did ask a lot of questions, ranging from basic-knowledge questions from folks newer to a particular topic, to quite advanced reflections. The talks were all really great, too, with the possible exception of my own, which was too jammed with rules and derivations. Anyhow, it was a very fun event, and I plan to ask for participant travel funds from NSF — which paid for this edition — in my future grant proposals. You can find the program, with titles and abstracts, and even a group picture, here.
Category Archives: Meetings
Last week I attended RDP 2013 in Eindhoven, the Netherlands. RDP 2013 consisted of two conferences, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications); and a number of workshops, of which I attended most of COS (Control Operators and their Semantics), which ran on the first and second days of RTA, and also the IFIP working group 1.6 on rewriting. My doctoral student Harley Eades and I each gave talks in COS, and I gave a talk in the working group meeting.
For me, attending this RDP was a really great experience. Everything ran really smoothly with travel, for starters. Flying from Cedar Rapids to Chicago to Amsterdam, and then taking a 1.5-hour train ride to Eindhoven, was easy and expeditious. The conference and hotel were just 5-10 minutes walk from the train station in Eindhoven, which was very convenient, too. The hotel was really quite nice, although like so many hotels I’ve stayed at, the wireless network was a bit flaky. Also, one had to know to request the remote control for the thermostat from the front desk — not something American travelers are expecting to have to do to operate the air conditioning unit. The local organization of RDP ’13 was also very good. There was a nice big building in which the meetings took place. The key organizational aspects, in my opinion, were that lunch was hosted on site (so time was not wasted wandering around for a restaurant in the middle of the day), and that there were lots of places to sit and do some work or talk with other participants. In my opinion the local organizers did a very good job with the meeting.
Anyhow, on to the technical side. COS was a great meeting to attend. There were invited talks by Matthew Flatt and Thomas Streicher. It is a testimony, perhaps, to the inherent interest of control operators that a single workshop could accommodate talks from such different parts of Computer Science. Matthew’s talk did a wonderful job explaining how control operators like call/cc, and an impressive catalog of related programming-language constructs, were useful in practice and complex to implement in combination with each other. I finally learned from Matthew’s talk what dynamic-wind is, which I had seen referenced in a couple papers. It is similar to try-catch-finally in Java, except that the semantics of dynamic-wind e1 e2 e3 is that we will execute e2, but whenever we do so, we will execute e1 before e2, and e3 after e2. The key point is that if exceptions are raised (or more generally, a continuation is called that takes us out of the context in which we are evaluating e2), then we will make sure to execute e3 before we execute the next thing after e2. So this is like the finally block of a try-catch-finally statement in Java. But intriguingly, it is also necessary to execute e1 whenever we re-enter computation of e2, which could happen by calling a continuation. This has no obvious counterpart in the Java construct. Thomas’s talk was about denotational categorical semantics related to control operators, using ideas from Krivine’s classical realizability (a form of compositional semantics for types which works for classical logic, and not just intuitionistic logic). It was a fun talk, because Streicher is a very engaging speaker. I am afraid that my category theory was not up to following what he had to say in detail, but I still enjoyed the talk as I caught glimmers of different interesting technical ideas in the categorical setting he is using.
And there were several other talks at COS ’13 quite relevant for our current work, in particular one by Kakutani and Kimura on the Dual Calculus with inductive and coinductive types. It seems that due to some fundamental issues which show up in the collapse of control categories for interpreting computational classical type theory (CCTT), it is difficult if not impossible to have inductive and coinductive types coexisting in the same CCTT. I can’t say I fully understand even how the categorical collapse (where the relevant category becomes just a pre-order, and there is at most one morphism from any source to any target object) leads to problems in the definition of the language. But it is a bit disturbing. Kakutani and Kimura proposed to tackle this by building up a restricted form of induction from coinduction, within the language. The treatment was again quite categorical. I would have to beef up my understanding of categorical semantics to understand what is happening here. We are working here at Iowa towards a similar goal, but using a type theory based on bi-intuitionistic logic instead of classical logic. It’s a matter for another post to give a real introduction to bi-intuitionistic logic, but the brief summary might be that it supports an operator dual to implication, which we call simply negative implication (the usual term is subtraction), where A negatively implies B is true in the current world (of a Kripke model) if there is an earlier world where A is false and B is true. The logic exhibits some classical features, but retains (we conjecture) canonicity for certain types.
At RTA and TLCA, I saw a number of really cool talks. Simon Peyton Jones gave a joint (between RTA and TLCA) invited talk about the “Core” intermediate language of Haskell, and how it uses explicit evidential expressions to show a simple type checker why expressions elaborated from Haskell input are indeed typable, without needing to invoke a complex type inference algorithm. The inference algorithm is earlier in the compiler pipeline, and generates these intermediate expressions with their evidential annotations. The evidence expressions are there to show why one type equals another, and they, with explicit annotations on lambda-bound variables, are sufficient to encode all the fancy typing features that Haskell programs use. And of course, Simon is a fantastic speaker, and his talk was, I am sure, a real highlight of the whole RDP.
I could go on and mention quite a few other talks I really enjoyed, on decreasing diagrams, strong normalization of System T using non-deterministic reduction, graph-isomorphism hardness of extended alpha-equivalence checking for letrec expressions, and more. These were all really stimulating. I want to mention a few other things that happened at the meeting, though. One that’s very important for us here is that the CoCo ’13 confluence-checking competition successfully ran using StarExec on Friday, June 28th. This is the first competition to use StarExec, and we were delighted (and relieved!) that CoCo ran smoothly on it, in real time during a workshop at RDP. The organizers, Harald Zankl and Nao Hirokawa, had a backup run they had already computed (with StarExec) offline, but fortunately they did not need to use it. So, this was great for them, and definitely great for StarExec.
One other thing that happened is that I was elected to the RTA Steering Committee (SC), during the business meeting for the conference. I am really appreciative of the warm reception the rewriting community has given me, and I feel a big responsibility to try to help guide the conference as a member of the SC. One immediate issue that is before the community is the question of pursuing a tighter connection with TLCA. Every two years the two conferences meet together as RDP (Rewriting Deduction and Programming). Next year, at the mighty FLoC ’14 in Vienna — itself just one component of the Vienna Summer of Logic (wow) — the conferences will be combined. The name will be “RTA/TLCA”, but there will be a single program committee, and a single track for submissions. I have to say that based on what I have seen so far, and talking also with others in the rewriting community at RTA, I am not sure a tighter merger — as in just a single conference — is a good idea. The problem is that while the two conferences share deep roots in lambda calculus and reduction semantics, they have gone in quite different directions. Most of the TLCA talks are about denotational semantics of typed languages, and many rely heavily on categorical constructions. This time there were only a couple TLCA papers, in my opinion, that were likely to be accessible to RTA attendees. Maybe I am wrong and more RTA folks are steeped in categorical semantics than I am guessing — but it seems a bit unlikely, at least judging by the typical RTA papers, which are much more focused on reduction semantics. The traditional problems of confluence and termination, as well as other algorithmic questions related to term-rewriting systems — like approximating the set of terms reachable by rewriting from an initial set of terms using a set of rules, or unification algorithms for various theories — are more the focus of RTA. Denotational semantics does not play much of a role. So, I am a bit worried that a combined conference will not be too successful. At FLoC it won’t matter, I think, because people can come and go from one meeting to another, so the audience will be quite dynamic. But if there were only an RTA/TLCA by itself, I think half the talks would not be accessible or interesting to half the audience, all the time. So I think I’m not in favor of combining more tightly than the RDP joint conference. But we will see how the discussions go.
Alright, hope all you who are reading this are having a good summer so far. Till next time.
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.
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.
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.
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).