  We prove that the variety of nuclear implicative semilattices is locally
finite, thus generalizing Diego's Theorem. The key ingredients of our proof
include the coloring technique and construction of universal models from modal
logic. For this we develop duality theory for finite nuclear implicative
semilattices, generalizing K\"ohler duality. We prove that our main result
remains true for bounded nuclear implicative semilattices, give an alternative
proof of Diego's Theorem, and provide an explicit description of the free
cyclic nuclear implicative semilattice.
