The paper submitted to Typed Lambda Calculi and Applications has been rejected. Again, all of the commentary was spot on. Our notation was not introduced well; the notation we used was odd; things were not explained properly. There is a consistent problem in our write-ups of trying to fit too much into a paper. We do have a lot to present: the syntax, the logic of safety, the type checking, the type inference, the operational semantics, the soundness proof, the completeness proof, the bounding argument, the relationship to previous works. It would be flat-out impossible to fit even a quarter of these into one conference paper, I would wager, but nonetheless it shouldn’t be too much trouble to write up a proper exposition that we can properly explain to people what we’re up to.

Two of our referees gave us a weak accept and honestly I felt bad for them since both of them obviously they put a lot of effort into it. Both of them agreed something worthwhile was being explained, but it was being explained too poorly.

In the meanwhile, I’m making slow and steady progress. Things will pick up once the term is over and I can forget about teaching for a while. I’m determined this won’t happen again.