Logic for Information Science A13
Prof. Keisuke Nakano
Assis. Prof. Kazuyuki Asada
Assis. Prof. Kentaro Kikuchi
KeywordsProgramming Language Theory, Formal Language Theory, Theorem Proving
Our ultimate goal is to fill a gap between humans and computers on programming. A human-readable description may put a burden on computers due to inefficient execution, while a computer-oriented (well-tuned) description may put a burden on humans due to knotty development. Our 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.
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 enables to 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 which keeps all the semantical properties of programs. Through the abstraction and mathematical analysis, we clarify 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.