Jason (jcreed) wrote,
Jason
jcreed

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
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments