コバヤシ サトシ   KOBAYASHI SATOSHI
  小林 聡
   所属   京都産業大学  情報理工学部 情報理工学科
   職種   教授
言語種別 英語
発行・発表の年月 1997/03
形態種別 研究論文
査読 査読あり
標題 Monad as Modality
執筆形態 単著
掲載誌名 Theoretical Computer Science
掲載区分国外
出版社・発行元 Elsevier
巻・号・頁 175(1),pp.29-74
総ページ数 46
著者・共著者 Satoshi Kobayashi
概要 In 1989, Eugenio Moggi proposed a general categorical framework for program semantics based on the notion of (strong) monads. Since his construction was not in harmony with categorical semantics of modal logics, he thought that Curry-Howard correspondence does not hold between constructive proofs in modal logics and programs. However, contrary to his thought, we can generalize his semantics and make it compatible with modal logic semantics. Moreover, we show that Curry-Howard correspondence actually holds. Using this result, we can extract monad-based imperative functional programs from constructive proofs in modal logics.
DOI 10.1016/S0304-3975(96)00169-7
ISSN 0304-3975