コバヤシ サトシ   KOBAYASHI SATOSHI
  小林 聡
   所属   京都産業大学  情報理工学部 情報理工学科
   職種   教授
言語種別 英語
発行・発表の年月 1997/03/30
形態種別 その他
標題 Monad as modality
執筆形態 その他
掲載誌名 Theoretical Computer Science
出版社・発行元 Elsevier
巻・号・頁 175(1),pp.29-74
著者・共著者 Satoshi Kobayashi
概要 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 ℒ-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 ℒ-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 ℒ-strong monads.
DOI 10.1016/S0304-3975(96)00169-7
ISSN 0304-3975