Computer and Mathematical Sciences
Logic for Information Science A13
KeywordsProgramming Language Theory, Formal Language Theory, Theorem Proving
Filling a gap between humans and computers
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.
-
Experimental result that illustrates effect of a program transformation based on formal tree language theory (where both time and space efficiency are improved in comparison with an existing implementation)
-
Coinductive formalization of validity of toss juggling patterns and its certification in the Coq proof assistant