At lunch Tobias Nipkow talked about verified decision procedures for various theories stemming from quantifier elimination procedures. The thing I took away from it was this lovely notion of "virtual substitutions" which remind me faintly of "leftist substitutions" --- they're kind of substitutions, but kind of not. In his case, you might substitute infinite or infinitesimally-different-from-known-thi
After that Anders and I talked unification for a couple hours. I think we went through almost verbatim (with him proposing and me counterexample-producing) all the major failed ideas I had about invariants for the placeholder-based HOU algorithm I came up with, leading right up to the one that worked. He still had some remaining ideas, but I feel good having transmitted the knowledge that I had gained by banging my head against the wall all those months.
David Baelde gave a talk about Bedwyn. Neat stuff, though I am having a continued crisis of faith about what it means to have inductive types in a logic.
Went out to dinner with people kinda late, talked a bit about co-Twelf and termination metrics.
