I guess it makes sense, his most recent papers are about indeterminism (http://www.pitt.edu/~belnap/futurecontingents.pdf), which logic doesn't handle well, but I'm not quite sure how you'd represent the branching-universe model he uses in a type system. I guess you'd need the history operator he uses, m/h = moment m on history h.