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.
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.
-
(no subject)
After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…
-
(no subject)
Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…
-
(no subject)
Finally the end is in sight for unpacking my books. Heartstrings are pulled over the desire to slim down and get rid of some of them, but so many are…
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments