Hi Steve,

Here are some refs.

Alechina, N., de Paiva, V. C. V. and Ritter, E. (1997) Relating Categorical and Kripke Semantics for Intuitionistic Modal Logics. Unpublished report, School of Computer Science, University of Birmingham. 

Benton, N., G. Bierman, and V. de Paiva. 1998. Computatational Types From a Logical Perspective. Journal of Functional Programming 8(2). 

Benton, P.N. and Wadler, P. (1996) Linear logic, monads and the lambda calculus. Proceedings of Symposium on Logic in Computer Science. 

Bierman, G. M., and V. de Paiva. 1996. Intuitionistic necessity revisited. Technical Report CSR-96-10. University of Birmingham, School of Computer Science, June.

Bierman, G. M. (1995) What is a categorical model of intuitionistic linear logic? Proceedings of 2nd International Conference on Typed Lamba-calculi and Applications: Lecture Notes in Computer Science 902, pp.78-93. Springer-Verlag.

Kobayashi, S. 1997. Monad as modality, Theoretical Computer Science 175:29 Ð 74.

Moggi, E. (1989) Computational lambda-calculus and monads. Proceedings of Symposium on Logic in Computer Science. pp.14-23. 

Moggi, E. (1991) Notions of computation and monads. Information and Control, 93(1):55-92.


Cheers,
Jeff