• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

プログラム言語における型の論理

研究課題

研究課題/領域番号 02249209
研究種目

重点領域研究

配分区分補助金
研究機関龍谷大学

研究代表者

林 晋  龍谷大学, 理工学部・数理情報学科, 助教授 (40156443)

研究期間 (年度) 1990
研究課題ステータス 完了 (1990年度)
配分額 *注記
700千円 (直接経費: 700千円)
1990年度: 700千円 (直接経費: 700千円)
キーワードプログラム言語における型理論 / プログラム検証
研究概要

型と論理式、プログラムと証明の対応によるプログラムの形式的開発において、プログラムが満足できる程度の自然なプログラムの開発ができる型理論の研究の一環として、従来の型理論や、林のPXシステムにおける仕様記述の方法を拡張した型理論ATT(A Type Theory)の設計と、その基本的性質の解明を行った。
ATTの特徴は、従来の型理論の最大の特徴とされていたふたつの型πxeA.B(依存積)とΣxeA.B(依存和)を廃し、simpley typed lambda calculusの型であるA→B,A×B,型の族のunionとintersection、および、singleton type {M}_Aを導入したことである。この結果、ATTでは、依存和、依存積は、基本的型構成子ではなく、ユ-ザ-によって定義させた派生的型構成子となった。従来の型理論では、依存和、依存積を、あまりに多義的に用いていたため、不自然な使い方を余儀なくされていた。例えば、プログラムの実行に関連のない証明のコ-ドを、プログラムの一部として取り込まざるをえない等の欠点は、このことに起因する。ATTでは、依存和,依存積を、より基本的を型に分解したため、プログラムの自然な意味にあった詳細な仕様記述がおこなえるようになったばかりでなく、従来の方法では不可能な仕様記述も行なえるようになった。
ATTは、当初,MartinーLo^^°fの型理論に基づいていたが、本年度の後半の研究により、Calculus of Contructionに基づく型理論に変更した。

報告書

(1件)
  • 1990 実績報告書
  • 研究成果

    (4件)

すべて その他

すべて 文献書誌 (4件)

  • [文献書誌] 高山 幸秀・林 晋: "Extended projection method with KreiselーTroelstra realizability" Information and Computation.

    • 関連する報告書
      1990 実績報告書
  • [文献書誌] 八杉 満利子・林 晋: "A functional system with transfinitely defined types" 日本数学会1991年春季総合分利会.

    • 関連する報告書
      1990 実績報告書
  • [文献書誌] 井田 哲雄編: "続 新しいプログラミング・パラダイム" 共立出版, (1990)

    • 関連する報告書
      1990 実績報告書
  • [文献書誌] 林 晋・小林 聡: "構成的プログラミングの基礎" 遊星社, (1991)

    • 関連する報告書
      1990 実績報告書

URL: 

公開日: 1990-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi