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

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • 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 

    Help
  • 2 comments