Jason (jcreed) wrote,

Today's ConCert meeting was pretty good. Every time I hear another angle on Noam's take on focusing, it makes a little more sense - Dan Licata seemed to expect to get more said, but I'm glad he slowed down to the audience's ability to understand. Then some conversations (re: focusing, qcqi, etc.) spilled out into the hallway, which were also quite fun.

Finished revising that intuitionistic letcc paper, submitted it again. Never going to be totally satisfied with that business, but at least it's formalized.

At D's I sketched the diagram from here for marymcglo. I think she appreciated it.

Re: unification: After days of hoping some successful alternative to the broken pile of inductive invariants would magically pop into my head, at least some candidate alternative did magically pop into my head as soon as I got home. The thing I hadn't considered before choosing how to quantify over instantiations of evars independently for evars appearing in terms and types ~ if this idea works out, it would explain perfectly why I've been struggling with invariants that always seem wrong at one end or the other of the proof.
Tags: social, talks, work

  • (no subject)

    Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

  • (no subject)

    Did some personal archaeology. Helped a little with laundry. Threw some chicken, onions, tomato, stock, peppers in the slow cooker and hopefully…

  • (no subject)

    Dinner with akiva and dannel at nuevo portal in carroll gardens. Ate a pile of chicken stew and rice and beans and maduros, good times. I do miss…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded