Naoki Kobayashi

He was born in 1968, and received his B.S., M.S., and D.S. degrees from University of Tokyo in 1991, 1993 and 1996, respectively. He is a professor in Graduate School of Information Sciences, Tohoku University. His current major research interests are in principles of programming languages. In particular, he is interested in type systems and static analysis of functional and concurrent programming languages.

Current Research Topics

• Type-Based Program Analysis and Transformation

  Type systems play an important role in guaranteeing partial correctness of programs. By enriching standard types with various information about program behavior, we can analyze a variety of properties of programs. Our recent work include:

  • Type-Based Analysis of Concurrent Programs

    Concurrent programs are hard to read, write, or debug. We have been studying type systems for statically checking behavior of concurrent programs. In particular, we have developed type systems for finding which communication or synchronization is guaranteed to succeed. Based on that work, we have implemented a type-based program analysis tool TyPiCal.

  • Type-Based Analysis of Resource Usage

    Resources such as files, memory, and network usually are associated with certain protocols. For example, a file should be eventually closed, and it should not be accessed afterwards. A lock that has been acquired lock should be eventually released. We are studying type-based methods for statically verifying that a program conforms to such resource usage policies. See our TOPLAS paper.

  • Type-Based Program Transformation

    Recent studies include type-based transformation of XML tree processing programs into XML stream processing programs (see our papers in APLAS 2004 and LOPSTR 2005), and type-based methods for useless-code elimination (see see our papers in Higher-Order and Symbolic Computation and APLAS2003).

  • Type-based Static Memory Management We have been studying linear type systems and region-effect systems for statically analyzing memory access and automatically inserting memory allocation/deallocation primitives (which correspond to malloc/free in C). See our APLAS2004 paper and POPL99 paper.

• Application of Theorem Provers (or Proof Assistants) to Program Verification

  I have been collaborating with Reynald Affeldt to develop a Coq library for verification of conurrent programs.

Selected Publications

Software

• TyPiCal: A TYpe-based analyzer for the PI-CALculus

Academic/Research Activities

• SAS 2009: PC member
• FOSSACS 2009: PC member
• APLAS 2008: PC member
• Recent Past Events: LICS 2008: PC member, SAS2007: PC member, FMOODS2007: PC member, APLAS2006 : PC Chair, TLDI 2007 : PC member, SAS2006: PC member FCS'05 : PC member, APLAS2005 : PC member, FOSSACS2005 : PC member, POPL 2005 : PC member, FLOPS 2004 PC member, FCS'04 PC member, CONCUR'03 PC member, PEPM'03 PC member, ASIAN 2003: PC member PADL'03 PC member, FOOL 10 PC member, TACS 2001 PC Co-Chair, ICFP 2001 PC member, PPDP2000 PC member, HLCL'00 PC member, IFIP TCS2000 PC member, FOOL 7 PC member, PPL 2000 PC Co-Chair

Information about Lectures(in Japanese)

Award

• 2001 IFIP TC2 Manfred Paul Award
• 2001 IPSJ Sakai Special Researcher Award
• 2003 IBM Japan Science Prize
• RTA 2008 Best Paper Award (Naoki Kobayashi and Hitoshi Ohsaki, "Tree Automata for Non-Linear Arithmetic")

To Foreign Students Who Wish to Join Our Research Group as Master students, PhD students, or Research Students: Read this first.

Home Page of Our Research Group

Graduate School of Information Sciences, Tohoku University

ECEI (Group of Electrical Engineering, Communication Engineering, Electronic Engineering, and Information Engineering) home page

Yonezawa's research group at Univeristy of Tokyo

E-mail: