Jason (jcreed) wrote,
Jason
jcreed

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.
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 

  • 1 comment