- >> Computing System Platforms Division
-
Computing Information Theory
Researcher
- [ Professor ]
Keisuke Nakano - [ Assistant Professor ]
Kazuyuki Asada - [ Assistant Professor ]
Kentaro Kikuchi
Group Web Site
https://www.ipl.riec.tohoku.ac.jp/dokuwiki/en/start
Research Activities
Our ultimate goal is to fill a gap between humans and computers. 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 well-tuned complicated programs work as humans intend.
Computing Information Theory(Prof. Nakano)
Research topics
- Theory of tree automata and tree transducers
- Program transformation and program verification
- Formalization in proof assistants
- Elucidation of computational behavior over combinatory logic
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 extending 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 semantical properties of programs, while the formal language technique above abstracts just specific aspects of programs, depending on purposes. Through the abstraction and further mathematical 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.
