研究室公開
OPEN LABORATORY
先進マルチメディア情報知能システム
情報工学コース
05
「ちゃんと動くコンピュータ」のために
数学的理論にもとづくソフトウェアづくり
|
住井・松田（一）研究室 |
EXHIBIT
オープンキャンパスでの展示
コンピュータ・ソフトウェアについて数学的に考える
携帯電話やゲームから金融、医療、自動車に至るまで、世の中のすべてのコンピュータは「プログラム」に従って動いています。プログラムが間違っていればコンピュータは正しく動きませんし、逆にプログラムさえ書けば良いことも悪いこともできます。この展示では「再帰」により「フラクタル図形」を描いたり、「なりすましメール」を送るプログラムとともに、プログラムの「正しさ」を数学的に「証明」等するための理論や技術の研究を紹介します。
私たちの研究
LABORATORY
関数型プログラミング
簡単・安全かつ強力なプログラミング手法・言語として近年になり再注目されている関数型プログラミングおよび関数型言語について、トップレベルのプログラマ・技術者・研究者らと共に、世界的に著名なプログラミングコンテストの主催を担当するなど、幅広い社会的活動を行っています。
スマートコントラクト検証手法の開発
スマートコントラクトプラットフォームはブロックチェーン技術に支えられた分散型のコンピューティング環境です。従来の分散型環境との大きな違いはその非中央性-管理者の不在性-にあります。これによりサービスに不具合が生じた際に管理者が対処するという従来の方法をとることが難しくなっています。我々はこうした状況の下スマートコントラクトを用いたアプリケーションの安全性を保証する技術の研究をプログラミング言語・手法の観点から行っています。
双方向変換
ソフトウェア開発においては、変換とその「逆変換」の実装がしばしば要求されます。また，そういった変換と逆変換の組は，パソコン・スマートフォンなどで様々な形式のデータを共有・同期するためにも有用です．我々は「ちゃんと動く」双方向変換記述のためのプログラミング言語・手法を開発しています。