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)
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.
- Theory of tree automata and tree transducers
- Program transformation and program verification
- Formalization in proof assistants
- Elucidation of computational behavior over combinatory logic