Jason (jcreed) wrote,

A series of recent breakthroughs on the research front. I have a crazy five-bullet-point definition of a certain property that can be enjoyed by a tuple of two contexts, a variable, a type and a substitution, a handful of lemmas that let me transfer knowledge of the property holding around in various ways, and one of the inductively maintained bullet points is exactly what I need for the big-mother soundness proof. I think. I hope.

Yesterday morning, neglected to mention went out to fuel & fuddle for tasty brunch with martin, tom7, sally, adam, pete. The service was slow as balls, though. Martin wanted to check out the renovated basement of the UC, so we did that. Played a game of DDR on the machine there. I still pretty much suck at it, but it's kinda fun. Tom7 drove adam, martin and I over to Paul's CDs. I picked up brubeck's "Time Out" because it caught my eye and I was appalled at myself for not owning it already. Went back home and played some other miscellaneous video games while waiting for ben to pick up martin.

The evening consisted mostly of work and talking to Donna about her work. Refinement types are a good deal more confusing than I thought.

  • (no subject)

    Still watching "Hell on Wheels". The characters motivations frequently make no sense at all, but at least they killed off the by-far most annoying…

  • (no subject)

    Watched some more "Hell on Wheels". Second season got dark fast.

  • (no subject)

    Tried watching ep 1 of "Hell on Wheels", which my dad recommended. It has a vaguely Deadwood feel, although the dialogue doesn't obviously sparkle…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment