Jason (jcreed) wrote,

Trying to work out the classical/intuitionistic thing for the first-order dependent case. In the course of doing this I've made what I think is the tallest prooftree I've ever made: 17 proof rules, no branching. It demonstrates that
cent(λq.q(λvw.v(λu.u(λry.w<r,λz.z(λx.y x)>))))
has type
C((Πx . A(x)) cont → Σx.(A(x) cont))

  • (no subject)

    Oh jeez Boulet, this is what you casually slap together for a 24-hour comic? Come on, now, you're just showing off. (But seriously it is so cute)

  • (no subject)

    I really liked this multiple choice test full of nonsense words that was solveable only on the basis of metagaming the questions. This is not…

  • (no subject)

    So Donald Barthelme apparently is back from the dead and writing craigslist missed connections: http://newyork.craigslist.org/brk/mis/3985247459.html

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded