中野 圭介教授菊池健太郎助教本研究室の究極的な目標は人間と計算機の間の隔たりを埋めることである。人間が計算機に命令を行う方法としてプログラムを記述する方法があるが、人間と計算機の思考には隔たりがある。人間に合わせた記述では実行効率が下がり計算機に負担がかかってしまい、計算機に合わせた記述では開発効率が下がり人間に負担がかかってしまう。そこで、人間に合わせた記述から計算機に合わせた記述を導く研究や、計算機に合わせた記述が人間の意図に沿っているかを証明する研究に取り組んでいる。本分野では、プログラムや計算を抽象化した構造について多くの成果を残している形式木言語理論を対象に研究を進めている。具体的には、木トランスデューサとよばれる木構造から木構造への変換に関する理論を精査し発展させることにより、効率的なプログラムを導出したり、プログラマが望む計算の性質を保証したりする枠組みの開発に取り組んでいる。また、定理証明支援系とよばれる計算機によって証明の正しさを検査するシステムを用いた研究も進めている。また、プログラミング言語意味論の研究も行っている。上述の形式言語技術が目的に応じてプログラムの一定側面のみを抽象するのに対し、こちらの手法ではプログラムの本質的な意味を全て保持した抽象化を行い、それを数学的に分析することにより、対象となるプログラミング言語の本質を明らかにする。具体的には、表示的意味論・操作的意味論・公理的意味論・圏論的意味論などがあり、プログラミング言語の理論的設計や前述の形式言語理論の技術と組合せプログラム検証などに応用する。浅田 和之助教図２ 定理証明支援系による「ジャグリングの数学」の形式化32Keisuke NakanoProfessorKentaro KikuchiAssistant Professor図１ プログラム変換による効率化Fig.1 Performance Improvement by Program TransformationKazuyuki AsadaAssistant ProfessorOur ultimate goal is to fill a gap between humans and com-puters. Humans describe a program for instructing computers what they should do. However, there is a gap between humans and computers. A human-readable description may put a bur-den on computers due to lengthy and inefficient execution, while a computer-oriented (well-tuned) description may put a burden on humans due to lengthy and inefficient development. Our research goals are to derive a well-tuned program from a human-readable description and to certify that well-tuned com-plicated programs work as humans intend.Our research focuses on formal tree language theory which succeeds in having many nice results for abstracted programs and computations. Specifically, we are investigating and extend-ing a theory of tree transducers, that is a formal model of tree-to-tree transformation, to develop a framework which enables to automatically derive efficient programs and statically certify properties desired by programmers. Additionally, we employ a proof assistant tool that can check the correctness of the proof by computers.We also study semantics of programming languages. This gives also a kind of abstraction of programs, which keeps all the se-mantical properties of programs, while the formal language technique above abstracts just specific aspects of programs, de-pending on purposes. Through the abstraction and further math-ematical analysis, we clarify the essence of a target programming language. This includes denotational, operational, axiomatic, and categorical semantics; and is applied to a theoretical design of programming languages, as well as to program verification by combining with the formal language techniques above.Research ActivitiesComputing Information Theory (Prof. Nakano)Fig.2 Formalization of Mathematical Juggling in CoqStaffコンピューティング情報理論研究室Computing Information Theory研究活動コンピューティング情報理論研究分野｜中野教授
元のページ ../index.html#34