What logic correponds via Curry-Howard to a Monad?
The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's A Judgmental Reconstruction of Modal Logic, which gives a constructive proof theory for S4 modal logic with box and diamond, and then translates Moggi's metalanguage into it.

Both papers note that the axioms of a strong monad were originally introduced by Curry in 1952, which was independently re-invented by Fairtlough and Mendler as lax logic. Giving the action on types and contexts below, we see:

$$
\begin{array}{lcl}
( \to )^+ &amp; =&amp; ◻^+ \to ^+ \\
(◯)^+ &amp; = &amp; ◊◻^+ \\
^+ &amp; =&amp;  \;\;\mbox{for atomic}\;  \
\end{array}
$$

The translation of Davies and Pfenning is very similar to Gödel's embedding of intuitionistic logic into classical logic, and to Girard's embedding of intuitionistic logic into linear logic.