Computer and Mathematical Sciences

Logic for Information Science A13

  • Prof. Keisuke Nakano      
  • Assis. Prof. Kazuyuki Asada      
  • Assis. Prof. Kentaro Kikuchi    
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