Jason (jcreed) wrote,
Jason
jcreed
It was a day. Advisor meeting went okay. I am feeling less doomed for having, for all practical purposes, signed away my soul as a proof irrelevance monkey for some time the moment I started my senior thesis, since it really looks like an interesting corner of the whole logic-type-theory curry-howard tangle. It's not so much an exotic modality, I think, as just a way of sneaking equational theory in the back door. Or maybe it just captures what you really want when you do propositions-as-types, or as in Awodey and Bauer's paper title, propositions-as-[types]. Anyway, I feel pretty confident that it's something. Yeah.

But I have some stuff to chew on for a while, and I think I'll try to submit to TPHOLs for real this time around.

Not a terrible lot else going on. Went to classes, aleksey's talk, got roped into doing puzzlestorm saturday. Asked the algebraic topology prof if all groups arise as fundamental groups of some space (I thought they did) but he didn't know off-hand.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    switch
    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    Help
  • 3 comments