コバヤシ サトシ   KOBAYASHI SATOSHI
  小林 聡
   所属   京都産業大学  情報理工学部 情報理工学科
   職種   教授
言語種別 日本語
発行・発表の年月 1993
形態種別 研究論文
標題 モナド・様相とCurry-Howard原理
執筆形態 単著
掲載誌名 日本ソフトウエア科学会第10回大会論文集
掲載区分国内
出版社・発行元 日本ソフトウエア科学会
巻・号・頁 225-228頁
総ページ数 4
著者・共著者 小林聡
概要 E. Moggiは1989年の論文で、モナドと呼ばれる圏論的概念を用いて、非決定性や副作用を含み得る一般化された$\lambda$計算に対する統一的な意味論を与えた。Moggiは彼の用いた圏が様相論理の意味論には適合しないことから、構成的論理の証明と一般化された$\lambda$計算の間にCurry-Howard対応は成立しないと考えた。しかし、Moggiの意味論はある変形によって様相論理に適合させられること、また、Curry-Howard対応も実は成立することを本発表で示す。