Monad as modality. (English) Zbl 0895.03011

Summary: In 1989, Eugenio Moggi proposed a categorical framework for program semantics based on the notion of a strong monad. He showed that various kinds of computation can be modeled in his framework. On the other hand, strong monads are not suited for the categorical semantics of traditional modal logics. According to these observations, Moggi thought that the Curry-Howard correspondence would not hold between programs and constructive proofs in modal logics. However, contrary to his view, we can show that proofs in a certain kind of modal logics are actually considered as programs. In this paper, first we shall introduce the notion of an \({\mathcal L}\)-strong monad which is a generalization of strong monads. Using this new notion, we can generalize Moggi’s semantics-preserving soundness and completeness with respect to his equational logic. Next we shall show that \({\mathcal L}\)-strong monads give a sound and complete semantics of a constructive version of S4 modal logic. Finally, we present a method to extract a monad-based imperative functional program from a proof in the modal logic. Interestingly, this method can also be understood in terms of \({\mathcal L}\)-strong monads.


03B70 Logic in computer science
68Q55 Semantics in the theory of computing
03B45 Modal logic (including the logic of norms)
03G30 Categorical logic, topoi
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
Full Text: DOI


[1] Bierman, G. M.; de Paiva, V. C.V, Intuitionistic necessity revisited, (Technical Report CSRP-96-10 (June 1996), School of Computer Science, University of Birmingham) · Zbl 0963.03033
[2] Brookes, S.; Geva, S., Computational comonads and intensional semantics, (Applications of Categories in Computer Science. Applications of Categories in Computer Science, London Mathematical Society Lecture Notes Series, Vol. 177 (1992)), 1-44 · Zbl 0797.18004
[3] Goldblatt, R., Logics of Time and Computation, (CSLI Lecture Notes No. 7 (1992), University of Chicago Press, Center for the Study of Language and Information), (revised and expanded) · Zbl 0635.03024
[4] Kock, A., Strong functors and monoidal monads, Arch. Math., 23, 113-120 (1972) · Zbl 0253.18007
[5] MacLane, S., Categories for the Working Mathematician (1971), Springer: Springer Berlin
[6] Moggi, E., Computational lambda-calculus and monads, (Proc. IEEE Symp. on Logic in Computer Science (1989)) · Zbl 0716.03007
[7] Moggi, E., Notions of computation and monads, Inform. Comput., 3, 55-92 (1991) · Zbl 0723.68073
[8] Nishizaki, S., Programs with continuations and linear logic, (TACS’91: Theoretical Aspects of Computer Software (1991), Springer: Springer Berlin), 513-531 · Zbl 07572016
[9] Pitts, A. M., Evaluation logic, (Birtwistle, G., IVth Higher Order Workshop. IVth Higher Order Workshop, Banff 1990. IVth Higher Order Workshop. IVth Higher Order Workshop, Banff 1990, Workshops in Computing (1991), Springer: Springer Berlin), 162-189
[10] Troelstra, A. S.; van Dalen, D., (Constructivism in Mathematics, Vol. II (1988), North-Holland: North-Holland Amsterdam) · Zbl 0661.03047
[11] Wadler, P., Comprehending monads, (ACM Conf. on Lisp and Functional Programing (1990)) · Zbl 0798.68040
[12] Wadler, P., The essence of functional programming, (Proc. 19th ACM Symp. on Principles of Programming Languages (1992))
[13] Wijesekera, D., Constructive modal logics I, Ann. Pure Appl. Logic, 50, 271-301 (1990) · Zbl 0714.03016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.