I think I need a gadget along the lines of an operad enriched over the category of bounded lattices. But I'm having trouble thinking through what features enrichment would correspond to in an internal language. What does it mean to have the internal language of an enriched category?
Thinking about say a basic linear lambda calculus with additive conjunction you would want a syntax something like:
$$ \tau \mathrel{::=} \textbf{I} \mid \tau \otimes \tau' \mid \tau \multimap \tau' $$
$$ e\mathrel{::=} \textbf{tt} \mid e ; e' \mid e, e' \mid \lambda x\colon \tau. e \mid e e' \mid \top \mid \bot \mid e \wedge e' \mid e \vee e' $$
where you just glom on the extra operations provided by the category you've enriched in.
And you want most operations to be some kind of homomorphism. I would expect equations along the lines of
$$ \bot, e = \bot $$ $$ e, \bot = \bot $$ $$ (e_1\wedge e_2), e_3 = (e_1, e_2) \wedge (e_2, e_3)$$
There's also an extra degree of freedom where you maybe want lax maps instead something like
$$ (e_1, e_2) \wedge (e_3, e_4) \vdash (e_1 \wedge e_3, e_2 \wedge e_4) $$
I guess you want $-,-$ to correspond to a map
$$\text{BoundedLattice}(\mathcal{C}(x, a) \cdot \mathcal{C}(y, b) , \mathcal{C}(x \otimes y, a \otimes b))$$
where $\cdot$ could be any number of bifunctors.
But I'm not sure of the exact details.