研究内容

<ゼミ>
18年度藤田研究室のゼミの詳細は現在未定です。


<研究内容>
コンピュータサイエンスの礎となる論理学の立場から,関数型プログラミング言語(ラムダ計算),計算機支援による定理証明,ソフトウェアの検証などに興味を持って研究を行なっています.卒業研究のスタイルとしては,次のような話題について基本的理論的な文献を読み,関連するプログラムやシステムを作成しています。

(1) プログラムの型と論理式との対応関係

プログラム言語における型と論理式との対応関係は,カリー・ハワードの同型対応として知られています.そして,プログラムの生成や性質の解析などに応用されています.この同型対応関係を拡張して,より高機能なプログラミング言語の概念設計や性質の解析に適用できるような理論を確立していきます。
  •  カリー・ハワードの同型対応
  •  ラムダ式の型推論
  •  ラムダ計算に基づくプログラミング言語


  • (2) プログラム変換と抽象機械
    計算の"残りの部分"を指す継続を使ったプログラム変換は,コンパイルや最適化のための技術として研究されてきました.ここでは,ジャンプの機能を持つ関数型言語を対象としたプログラム変換,及び変換されたコードを実行する機械について考えていきます。
  •  継続に基づくプログラム変換
  •  抽象機械の設計


  • (3) Webグラフの構造解析
    Webページをノードとし,リンクを有向辺とするグラフはWebグラフと呼ばれて,情報検索に活用されています.Webグラフの構造的な特徴を抽出して,Web情報検索に役立てることを目標としたシステムの作成,実験や情報収集などを行います。
  •  Webグラフの作成
  •  バックリンク情報の収集と解析
  •  クラスタ,コミュニティーの発見

  •      Webグラフsample(起点:05'2/3現在の藤田研TOPページ、深さ:3)
           Webグラフ
           上記グラフのノード番号に対応するURL


    <参考書>
    • 情報科学のにおける論理:小野寛晰(日本評論社)
    • 計算理論 計算可能性とラムダ計算:高橋正子(近代科学社)
    • プログラム意味論:横内寛文(共立出版)
    • Linked: The New Science of Networks:A.-L.Barabasi (Perseus Publishing), 新ネットワーク思考:青木訳(NHK出版)
    Logic:
    • Logic and Structure --- Third Edition: Drik van Dalen (Springer)
    • Natural deduction, A proof-theoretical study: D.Prawitz (Almqvist&Wiksell)
    • Logic in Computer Science (2nd edition): Michael Huth and Mark Ryan (Cambridge University Press)
    Lambda Calculi:
    • Introduction to combinators and lambda-calculus: J.R.Hindley and J.P.Seldin (Cambridge University Press)
    • The Lambda Calculus --- Its Syntax and Semantics, Revied Edition: H.P.Barendregt (North-Holland)
    Curry-Howard isomorphism:
    • Proofs and Types: J.-Y.Girard, P.Taylor and Y.Lafont (Cambridge University Press)
    • The Lambda Calculi with Types: H.P.Barendregt in: Handbook of Logic in Computer Science Vol. 2 (Oxford University Press)