Adam Chlipala, "Syntactic Proofs of Compositional Compiler Correctness"
I liked this talk. By strengthening the induction hypothesis to quantify over the other compilers that might have compiled bits of your program, you get nice lean, syntactic modular proofs of compiler correctness that have some of the advantages of more high-powered semantic proofs that use logical relations to express compiled program equivalence.
Yu David Liu, "Task Types for Pervasive Atomicity"
Didn't really understand this talk. I fear there's part of my brain that shuts off when I hear the word "atomicity". I liked the general notion of radically different choices of defaults for defaults for programming languages, though --- I think one of the main ideas of this talk was to instead make "everything atomic with a few programmer chosen exceptions" rather than the current state of the art of making everything not atomic with a few programmer chosen exceptions.
Martin Hirzel, "Jeannie and Blink: Tools for Multi-Lingual Programming and Debugging"
Actually very nice use of color-coding and diagrams and stuff. The work was about compiling programs written in a language that lets you pass back and forth between Java and C by appropriate quoting operations in a way that reminds me of weave and tangle from literate programming. Naturally one pass slurps out the Java bits, and one pass slurps out the C bits, and you have one source file with fewer magic string constants and you can typecheck more things and life is wonderful. Interesting bit where you kind of have to closure-convert out Java and C environments, respectively, to pass around. Interesting to me I think in that it's closure-conversion with no particularly advertised notion of closures, although it's kind of like coroutines passing back and forth between the two langauges. The discussion of how they wrote a debugger that's compatible with both languages at once sort of lost me in the implementation details, but it sounds like interesting work too.
Lunch was delightfully unfancy sandwiches. Gossiped about separation logic and category theory and FPCC. There is a tower of the building we're in from which you can see reeeally far in all directions, a pretty lovely view.
David Naumann, "Region logic and dynamic encapsulation boundaries".
Reasoning about programs by allowing annotations that are little inline effectful updates to "ghost state" which never effects control flow but creates a nice abstract thing that is what you want to talk about through hoare triples to client code, rather than the implementation itself. One interesting thing is this sort of lifting operation that takes a field name, which leads to a very simple but strong, static notion of separation/separability along field name lines rather than along the lines I usually expect of natural modularity boundaries in a program. Like, if I have a class with fields x and y, surely I imagine that their values interact a lot in the course of the implementation of that class, yet surely I know that immediately after an assignment to an x in one object, no y-field of any object anywhere has changed.
Rob Dockins, "A Fresh Look at Separation Algebras and Share Accounting"
Talking about model theory of BI and separation logic and stuff. Ok, so separation algebras have enough operations to interpret separating conjunctions, but what are the axioms for? Especially cancellativity. Is there completeness after all? Dunno yet.
There is a positivity axiom: a * b = c → c * c = c → a * a = a which effectively forbids nontrivial units, i.e. negative elements. Equivalent to requiring substate relation (a substate of b iff b splits as a * c) is antisysmmetric. They also require "disjointness" a * a = b → a = b. Apparently disjointness implies positivity, but not the converse.
There is a "cross-split" axiom that requires that if you have two resource divisions, you can refine it to a four-way split. There is a highly surprising "dense" splitting axiom finally that says that any nonempty thing can be split into two nonempty things! Is this like fractional permissions? Ok, yes, sure seems to be. Oh, actually it seems to be about a whole basket of different (one might say) permission schemes with various different properties. Now he defines a separation algebra based on funny coinductive-ish-feeling tree structures that has basically every nice property every mentioned, including decidable equality. Pretty slick.
Ken Shan, ``Lifted inference: normalizing loops by evaluation''
Seems to be doing some delimited continuation magic to do loop
lifting optimizations in the programming language itself, rather than
in the compiler. The idea seems to be to some extent classic "debugging by delimited continuations" by making funny continuationy breakpoints, but then you do some symbolic evaluation to tell when the lifting optimization is allowed.
Qian Xi, "A Context-free Markup Language for Semi-structured Text"
I tragically dozed off during the motivation section because I already think PADS is a good idea, and then I sort of lost the thread. The phrase "substructural logic" got used at some point, and that woke me up, but I failed to see where she was doing any logic. Maybe I should look it up later and read it, it sounded like kind of interesting work. Oh! Wait, no here it is, it's related to relevance logic somehow. Too bad I don't get how exactly.
All in all a fun time, glad I went. My hit rate for understanding basically what was going on in talks was alarmingly high. Either my attention span is improving or they were generally good talks, and I suspect the latter.