  This paper introduces two sequent calculi for intuitionistic strong L\"ob
logic ${\sf iSL}_\Box$: a terminating sequent calculus ${\sf G4iSL}_\Box$ based
on the terminating sequent calculus ${\sf G4ip}$ for intuitionistic
propositional logic ${\sf IPC}$ and an extension ${\sf G3iSL}_\Box$ of the
standard cut-free sequent calculus ${\sf G3ip}$ without structural rules for
${\sf IPC}$. One of the main results is a syntactic proof of the
cut-elimination theorem for ${\sf G3iSL}_\Box$. In addition, equivalences
between the sequent calculi and Hilbert systems for ${\sf iSL}_\Box$ are
established. It is known from the literature that ${\sf iSL}_\Box$ is complete
with respect to the class of intuitionistic modal Kripke models in which the
modal relation is transitive, conversely well-founded and a subset of the
intuitionistic relation. Here a constructive proof of this fact is obtained by
using a countermodel construction based on a variant of ${\sf G4iSL}_\Box$. The
paper thus contains two proofs of cut-elimination, a semantic and a syntactic
proof.
