研究室公開
OPEN LABORATORY
先進マルチメディア情報知能システム
情報工学コース
05
「ちゃんと動くコンピュータ」のために
数学的理論にもとづくソフトウェアづくり
|
住井・松田研究室 |
EXHIBIT
オープンキャンパスでの展示
コンピュータ・ソフトウェアについて数学的に考える
携帯電話やゲームから金融、医療、自動車に至るまで、世の中のすべてのコンピュータは「プログラム」に従って動いています。プログラムが間違っていればコンピュータは正しく動きませんし、逆にプログラムさえ書けば良いことも悪いこともできます。この展示では「再帰」により「フラクタル図形」を描いたり、「なりすましメール」を送るプログラムとともに、プログラムの「正しさ」を数学的に「証明」等するための理論や技術の研究を紹介します。
私たちの研究
LABORATORY
関数型プログラミング
簡単・安全かつ強力なプログラミング手法・言語として近年になり再注目されている関数型プログラミングおよび関数型言語について、トップレベルのプログラマ・技術者・研究者らと共に、世界的に著名なプログラミングコンテストの主催を担当するなど、幅広い社会的活動を行っています。
プログラム等価性証明手法
二つのプログラムの振る舞いが等価であるか否かは、プログラムの最適化や検証にも密接に関連する、基本的かつ重要な問題です。我々は「環境双模倣」に基づくプログラム等価性証明手法を考案し、幅広いプログラミング言語および計算モデルに適用しました。
双方向変換
ソフトウェア開発においては、変換とその「逆変換」の実装がしばしば要求されます。また，そういった変換と逆変換の組は，パソコン・スマートフォンなどで様々な形式のデータを共有・同期するためにも有用です．我々は「ちゃんと動く」双方向変換記述のためのプログラミング言語・手法を開発しています。