Jason (jcreed) wrote,
Jason
jcreed

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))
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 

  • 5 comments