HOME > Organization / Research > Nakano Laboratory

Organization / Research

Computing Information Theory [Nakano] Laboratory


photo Keisuke NAKANO, Professor (Photo)
Kazuyuki ASADA, Assistant Professor

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 burden 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 a well-tuned complicated program work as humans intend.

Our research focuses on formal tree language theory which succeeds in having many nice results for abstracted programs and computations. Concretely, we are investigating and extending a theory of tree transducers, which is a 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 to formalize our theory and mathematics.

Group of Electrical Engineering, Communication Engineering,
Electronic Engineering, and Information Engineering, Tohoku University
6-6-05, Aramaki Aza Aoba, Aoba-ku, Sendai, Miyagi 980-8579, Japan
TEL : 022-795-7186 (Japanese Only)
Email :