Summer, in currently damp and overcast form, is in full swing here in Iowa City, and nothing says summer like a grad seminar (actually, there’s an undergrad one running, too!). This summer, we are looking at papers on methods for proving termination of typed (terminating) lambda calculi. The (current) list of papers is below. The first three are co-authored by people in the group, and the last two are by others. I have posted previously on QA9 about the first two papers:
Hereditary Substitution for Stratified System F, by Harley Eades III and Aaron Stump.
Equality, Quasi-Implicit Products, and Large Eliminations, by Aaron Stump and Vilhelm Sjoeberg.
A Simple Ordinal Recursive Normalization of Goedel’s T (Citeseer link), by Paul Voda
Reducibility and TT-lifting for Computation Types, by Sam Lindley and Ian Stark.
We’re trying a different seminar format this summer than the one we have been using in our group. For each paper, we have a presenter, who presents the paper in the seminar meetings covering it; a responder, who comes prepared with at least three questions, observations, or points of some kind to raise; and a reporter, who will write up a paragraph or two on what was presented, after the seminar meetings on that paper. The goal is to cover more material than our usual round-robin reading-group format (where we take turns reading through text together during the meetings), while trying to make sure that more people than just the presenter understand the paper. The plan is to have the reporter post to QA9, so keep an eye out for those posts in coming weeks.