ブックタイトルGSIS_2019

概要

GSIS_2019

10情報基礎科学専攻Department of Computer and Mathematical Sciences■研究キーワード■■KEYWORDS ■Organization of an international functional programming An award for research on proof method of program equivalencecontest（ icfpc2011.blogspot.jp）国際関数型プログラミングコンテストの主催（icfpc2011. プログラム等価性証明手法の研究による受賞blogspot.jp）In today's society, many critical systems are controlled by computers: transportation safety, medicaldevices, commerce and public communication. The software that runs on those computers, however, isoften developed on weak foundations, which regularly causes it to behave in unanticipated and ratherundesirable ways.To develop the software we can rely on, based on solid logical and mathematical foundations, westudy programming languages, methods, tools and computational models. Our recent research topicsinclude:・ Proof techniques for program equivalence: The fundamental question underlying programoptimization and transformation is whether two programs behave the same. We have developedan “environment bisimulation” technique for proving program equivalence and applied it to a widerange of programming languages and computational models.・ Functional programming: Functional programming is gaining interest as a reliable, easy toreason and powerful programming method. Helping raise this interest is the annual internationalprograming contest, with world-wide participation by top-level programmers and researchers. Wehave served as the organizers of the 2011 programming contest.・ Bidirectional transformation: In today's distributed world, we often have to keep many sets of data insync: transforming from one set to another and back. We are developing programming languagesand techniques for correct-by-construction bidirectional transformations.Software that “works”現代では、パソコンや携帯電話は言うに及ばず、交通機関や電子政府、金融取引や医療機器など、社会の根幹や人命を左右するシステムがコンピュータにより制御されている。しかし、それらのコンピュータを実際に制御しているソフトウェアは、論理的・数理的な基礎の薄弱なまま、しばしば人的努力のみによって開発されており、そのことが現実にさまざまな問題を引き起こす主因となっている。本研究室では、このような問題に対処すべく、論理的・数理的基礎に基づいたソフトウェア開発のためのプログラミング言語・手法、ツール、計算モデル等に関する研究を行っている。以下は最近の研究テーマの例である．・プログラム等価性証明手法：二つのプログラムの振る舞いが等価であるか否かは、プログラムの最適化や検証にも密接に関連する、基本的かつ重要な問題である。我々は「環境双模倣」に基づくプログラム等価性証明手法を考案し、幅広いプログラミング言語および計算モデルに適用した。・関数プログラミング：簡単・安全かつ強力なプログラミング手法・言語として近年になり再注目されている関数プログラミングおよび関数型言語に関し、トップレベルのプログラマ・技術者・研究者らと共に世界的に著名なプログラミングコンテストの主催を担当するなど、幅広い社会的活動を行っている。・双方向変換：ソフトウェア開発においては，変換とその「逆変換」の実装がしばしば要求される。我々は「ちゃんと動く」双方向変換記述のためのプログラミング言語・手法を開発している。「ちゃんと動く」ソフトウェアProgramming Language Theory ／ Computation Models ／ Information Securityプログラミング言語理論／計算モデル／情報セキュリティhttp://www.sf.ecei.tohoku.ac.jp/Foundations of Software Scienceソフトウェア基礎科学教 授准教授助 教Prof.Eijiro SumiiAssoc. Prof.Kazutaka MatsudaAssis. Prof.Oleg Kiselyov住井 英二郎松田 一孝Oleg Kiselyov