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