Jason (jcreed) wrote,
Jason
jcreed
During type systems I daydreamed about adding exponentials back to BI, somehow. It seems like the well-known fact that things like box and bang want to express some sort of propositional validity (rather than mere truth) means that banged things in BI ought to have exactly the property that they are indifferent to being combined by ";" or ",", since being closed terms they should be immune to sharing anyway, and therefore not care what sharing constraints are put on them. Having a two-way rule of the form

Gamma(Delta, !A) |- B
=====================
Gamma(Delta; !A) |- B

as well as intro and elim rules seems really disturbing. ! has dereliction in linear, however. Hmm.

I finally moved some plates and forks into my office so eating isn't quite so ad hoc. Got a bunch of work done on the complexity theory homework. It's great when group work really works and people can fill in for each other's confusions and come up with n times as many attempts and ideas.

I stupidly went to Cyert looking for my stipend check and remembered they had already told us it wasn't there. By the time I got back to Wean it was past 5. I'll have to wait until tomorrow for my ph4t l3wt, I guess.
Subscribe

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • 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
  • 1 comment