It’s been a pretty busy summer for our group, and I want to give an update of some of the things we have been up to. Our biggest news is probably the great opportunities some group members have recently left to pursue:
- Duckki Oe accepted a postdoc at MIT, working with Adam Chlipala. The project is concerned with verification of system software, so that should be quite challenging and exciting.
- Garrin Kimmell accepted a position at Kestrel Institute. Kestrel is a well-known research institute that applies formal methods for developing reliable software systems, largely (as I understand) for government contracts.
Both of these positions will provide fantastic environments for Garrin and Duckki to continue developing their substantial formal-methods and programming-languages skills, with some of the top formal-methods researchers in the field. So, I am very, very happy about this (and so are they!).
Frank Fu and Harley Eades attended several interesting research events this summer — but I don’t want to steal their thunder: you can check out their reports on NASSLLI and ICALP on their blogs (see my blogroll).
We had an undergraduate researcher visiting here from Ohio State University, Angello Astorga. Angello was here through the Summer Research Opportunities Program (SROP), run by the CIC (Big Ten Schools + U. Chicago). This is a really great program that gives students from underrepresented populations a research experience, and a lot of mentoring and professional development activities, too. I know Angello was especially excited about the multiple practice GREs. Just kidding. It was truly a very good experience for the attendees, from what I saw. Students really did an impressive job mastering new material and presenting it at an end-of-the-summer undergrad research conference. They really knew their stuff, and did a very nice job explaining it. Angello was working here on verifying the CK machine for untyped lambda calculus using Trellys. He picked up lambda calculus and Trellys and completed (almost!) the verification in just 8 weeks, after just his sophmore year as a CS major at OSU. Wow! I was impressed. Here’s a picture of Angello with his poster. We are hoping he will present it at the upcoming Midwest Verification Days (MVD), hosted at Kansas U. September 20-21.
On the research side, I am very fired up about the Dual Calculus (due to Wadler). It is a really elegant and intriguing formalism. Hopefully I’ll manage to post more about it sometime soon. The most helpful source I have found so far is “Dual Calculus with Inductive and Coinductive Types” by Kimura and Tatsuta (sorry, no free PDF seems to be available, only at SpringerLink).
Hope your summer is ending well.