The variety of Grishin algebras is shown to be closed under MacNeille completion, and this is applied to embed an arbitrary Grishin algebra into the algebra of all propositions of some cover system, by a map that preserves all existing joins and meets.
This representation is then used to give a cover system semantics for a version of classical bilinear logic that has first-order quantifiers and infinitary conjunctions and disjunctions.