コバヤシ サトシ   KOBAYASHI SATOSHI
  小林 聡
   所属   京都産業大学  情報理工学部 情報理工学科
   職種   教授
言語種別 日本語
発行・発表の年月 1990
形態種別 研究論文
招待論文 招待あり
標題 構成的証明からのプログラム抽出
執筆形態 単著
掲載誌名 コンピュータソフトウェア
掲載区分国内
出版社・発行元 日本ソフトウエア科学会
巻・号・頁 Vol. 7(No.4),3-18頁
総ページ数 16
著者・共著者 小林聡
概要 近年、構成的数学の計算機科学への応用、特に、プログラムの仕様記述・検証・プログラム合成・型理論などへの応用が盛んに議論されるようになった。そのような応用の一つとして、構成的証明からのプログラムの抽出がある。そこで用いられる理論にはさまざまなものがあるが、特に重要と考えられるものはrealizability interpretation と構成的型理論であろう。本稿ではこれらの理論について両者の関連に留意しつつ解説する。
DOI https://doi.org/10.11309/jssst.7.4_319