Jason (jcreed) wrote,
Jason
jcreed

I am back in pittsburgh, at last, having arrived 37 and a half hours after I woke up saturday morning, with about 5 or 6 hours of acutal sleep at the HoJo in Newark. Sally and adam were kind enough to greet me at the airport and transport me back. Took a shower. Went to sam's with sal.

Didn't do a scrap of japanese during the week. Must get that done before tomorrow. But at the airport I did play around with a cute encoding of higher-order patterns in twelf (without requiring any linearity!) that seems to work okay. The trick is using natural-number tags to get back the single-use-in-a-spine-ness that an affine arrow would give you naturally. The nontrivial induction cases of correctness proofs are still eluding me, though, grr. Eta-conversion is once again the bane of my existence.
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 

  • 0 comments