ブックタイトルGSIS_2019

概要

GSIS_2019

12情報基礎科学専攻Department of Computer and Mathematical Sciences■研究キーワード■■KEYWORDS ■Our ultimate goal is to fill a gap between humans and computers on programming. A humanreadabledescription may put a burden on computers due to inefficient execution, while a computeroriented(well-tuned) description may put a burden on humans due to knotty development. Our goalsare to derive a well-tuned program from a human-readable description and to certify that well-tunedcomplicated programs work as humans intend.Our research focuses on formal tree language theory that can deal with abstracted computations.Specifically, we study a theory of tree automata and transducers to develop a framework which enablesto automatically derive efficient programs and statically check properties desired by programmers.Additionally, we use a proof assistant tool to certify the correctness of our theory.We also study semantics of programming languages. This gives a kind of program abstraction whichkeeps all the semantical properties of programs. Through the abstraction and mathematical analysis, weclarify the essence of a target programming language. We apply denotational, operational, axiomatic,and categorical semantics to a theoretical design of programming languages and program verification.Filling a gap between humans and computers本研究室の究極的な目標は，プログラミングにおける人間と計算機の隔たりを埋めることです．人間に合わせた記述では実行効率が下がって計算機に負担がかかり，計算機に合わせた記述では開発効率が下がって人間に負担がかかります．そこで，人間に合わせた記述から計算機に合わせた記述を導く「プログラム変換」や，計算機に合わせた記述が人間の意図に沿っているかを保証する「プログラム検証」に取り組んでいます．本研究室では，プログラムや計算を抽象化した構造を扱うことのできる「形式木言語理論」を中心に研究を進めています．具体的には，木オートマトンや木トランスデューサなどの理論に基づき，効率的なプログラムを導出したり，プログラマが望む計算の性質を保証したりする枠組みを開発しています．理論の正当性を確認するために定理証明支援系とよばれるツールを用いた研究も進めています．このほか，「プログラミング言語意味論」の研究も行っています．こちらの手法では，プログラムの意味をすべて保持した抽象化を行い，それを数学的に分析することにより，対象となる言語の本質を明らかにします．具体的には，表示的意味論・操作的意味論・公理的意味論・圏論的意味論などを，言語の理論的設計やプログラム検証に応用します．ヒトとコンピュータのギャップを埋めるProf.Keisuke NakanoAssis. Prof.Kazuyuki Asada中野 圭介浅田 和之Programming Language Theory ／ Formal Language Theory ／ Theorem Provingプログラミング言語理論／形式言語理論／定理証明https://www.ipl.riec.tohoku.ac.jp/Logic for information Science情報論理学教 授助 教Experimental result that illustrates effect of a program transformationbased on formal tree language theory (where both time and spaceefficiency are improved in comparison with an existing implementation)Coinductive formalization of validity of toss juggling patternsand its certification in the Coq proof assistant形式木言語理論に裏付けられたプログラム変換による効果を示す実験結果（既存の実装と比較して時間効率も空間効率も改善が見られる）ジャグリングのパターンの妥当性の余帰納的形式化および定理証明支援システムCoq によるその正当性の証明