Monad as modality.

*(English)*Zbl 0895.03011Summary: 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.

##### MSC:

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 |

##### Keywords:

program semantics; Curry-Howard correspondence; modal logics; generalization of string monads; equational logic; method to extract a monad-based imperative functional program from a proof
PDF
BibTeX
XML
Cite

\textit{S. Kobayashi}, Theor. Comput. Sci. 175, No. 1, 29--74 (1997; Zbl 0895.03011)

Full Text:
DOI

##### References:

[1] | Bierman, G.M.; de Paiva, V.C.V, Intuitionistic necessity revisited, () · Zbl 0963.03033 |

[2] | Brookes, S.; Geva, S., Computational comonads and intensional semantics, (), 1-44 · Zbl 0797.18004 |

[3] | Goldblatt, R., Logics of time and computation, (), (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 Berlin |

[6] | Moggi, E., Computational lambda-calculus and monads, () · 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, (), 513-531 |

[9] | Pitts, A.M., Evaluation logic, (), 162-189 |

[10] | Troelstra, A.S.; van Dalen, D.; Troelstra, A.S.; van Dalen, D., () |

[11] | Wadler, P., Comprehending monads, () · Zbl 0798.68040 |

[12] | Wadler, P., The essence of functional programming, () |

[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.