Dr. Keiko Nakata
Department: Computer Science
Visiting time at TU Darmstadt: April 2013 – Juni 2013
Teaching and research area: Programming Languages
Last academic station: Institute of Cybernetcis, Tallin, Estonia
Most important academic stations: Kyoto University; Institute of Cybernetics, Tallin; Conservatoire National des Arts et Métiers and INRIA Rocquencourt.
Teaching offer in the summer semester 2013: Mechanizing mathematical theory of programming languages: Operational semantics of WHILE in COQ.
1. Why should students of TU Darmstadt attend your lectures and/or seminars?
Modern society is dependent on the correct functioning of complex technical systems controlled by computers. To be trustworthy, they must behave as intended. Serious reasoning about trustworthiness of a computer system needs to be formal. Recent advances in proof assistants enabled the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof of the correctness. In my lectures, students will experience a flavor of the computer-assisted formal program verification, using a proof assistant Coq.
2. Why did you choose TU Darmstadt for your KIVA Visiting Professorship?
I am here for collaboration with the research group „Software Engineering“, led by Prof. Reiner Hähnle, at the Computer Science Department. I participated in the EU FP7 HATS project, coordinated by Prof. Hähnle, where we produced many exciting results together with other members from the consortium. With my KIVA visit, I would like to tighten my collaboration with Prof. Hähnle and his group in a broader context beyond the HATS project.
3. At TU Darmstadt and especially in the context of KIVA interdisciplinarity has a high importance. Which are the connections between your area of teaching and research to other thematic fields and disciplines?
My area of teaching and research has a strong connection to mathematics. For instance, technical advances in proof assistants are led by interdisciplinary research between computer science and mathematics. On the one hand, proof assistants are based on mathematical formalisms. On the other hand, using proof assistants for program verification explores the underlying formalisms, posing new mathematical questions. Type theory, the underlying formalism of Coq, is the one of the most successful examples: in the past few years, a new and deep connection has emerged between type theory and homotopy theory.
4. What is your perfect balance to a stressful working day?