For an application connected with the syntax-semantics interface in natural language, I would be grateful for either (1) advice on ways to complete the following proportion: cartesian closed category: positive propositional intuitionistic logic: heyting semilattice: Henkin frame (with products) :: biclosed (not necessarily symmetric) monoidal closed category: noncommutative multiplicative propositional intuitionistic linear logic: residuated monoid: ? or (2) a persuasive argument that there is no sensible way to complete it. Carl Pollard