Anyone know where the canonical reference is for practical programming with type inference in a BI-based type system?
I haven't tried looking very hard yet, because while doing so I turned up (and got distracted by) "Kripke Resource Models of a Dependently-Typed, Bunched λ-Calculus" by Ishtiaq and Pym (non-paywall citeseer link) and on page 7 they claim they can simulate LLF inside RLF somehow, which is quite a puzzler: RLF, as far as I can tell, and to the extent that I am right about this it is much to my chagrin, is not linear logic as the rest of the world understands it, but rather "relevant logic", where you require at least one use of each variable, instead of exactly one. My epistemic state about the paper is still such that Idunno if they are pulling some extra trick to get LLF encoded, but it's quite a surprising assertion.
