TOP > Research > Comprehensive List of Researchers "Information Knowledge" > Department of Information Engineering > Software Science and Technology Group >NAKAZAWA, Koji

Comprehensive List of Researchers "Information Knowledge"

Department of Information Engineering

Name
NAKAZAWA, Koji
Group
Software Science and Technology Group
Title
Associate Professor
Degree
Doctor of Science
Research Field
Theory of Programming Languages / Type Theory / Mathematical Logic

Current Research

Program analysis and verification based on relationship between programming languages and logical systems

Background: To analyze and verify programs rigorously, we have to give a mathematical definition for meaning of programs, and a lot of notions from mathematical logic have been used for that purpose. For example, the notion of “proofs" is adopted to define a behavioral character of programs (operational semantics), and to check some properties of programs (type systems and Hoare logic). Moreover, there is more direct relationship between programming languages and logical systems, known as Curry-Howard isomorphism. Under this correspondence, programs can be seen as proofs which ensures satisfiability of specifications of the programs.


Outline: We aim to analyze properties of programs and to study computational aspects of logics through the relationship between (type systems for) programming languages and logical systems. Moreover, we want to apply our theoretical results to program verification techniques.


Research topics:
1. Extension of Curry-Howard isomorphism: The Curry-Howard isomorphism were originally discovered as a relationship between the intuitionistic logic (a restriction of the classical logic) and a small programming language (the simply typed lambda calculus). It has been studied that an axiom of classical logic corresponds to the type of a control operator, and that some modal logic systems correspond to type systems for muti-staged programming. In particular, we are interested in studying computational aspects of classical logic.
2. Program verification with types: Type systems for programming languages are designed to guarantee that any typed program does not behave badly. Therefore, it is important to automatically check typability of programs. In fact, some real programming languages adopt automatic type checking (and type inference). However, if we naively add a sophisticated type such as polymorphic types and abstract data types, the type checking problem becomes undecidable. One of our research interest is to study a theoretical limit of type checking problem for such types.

Career

  • October 2015 – Present : Associate Professor
      Graduate School of Information Science, Nagoya University
  • December 2002 – September 2015 : Assistant Professor
      Graduate School of Informatics, Kyoto University
  • September 2009 – December 2009 : Visiting Researcher
      IRIT, Paul-Sabatier University (Toulouse III)

Academic Societies

  • JSSST
  • MSJ
  • EATCS

Publications

  1. Koji Nakazawa and Hiroto Naya. Strong reduction of combinatory logic with streams. Studia Logica, 103:375–387, April 2015.
  2. Koji Nakazawa and Tomoharu Nagai. Reduction system for extensional lambda-mu calculus. In 25th International Conference on Rewriting Techniques and Applications joint with the 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), volume 8560 of Lecture Notes in Computer Science, pages 340–363, July 2014.
  3. José Espírito Santo, Ralph Matthes, Koji Nakazawa, and Luís Pinto. Monadic translation of classical sequent calculus.Mathematical Structures in Computer Science, 23:1111–1162, December 2013.
  4. Koji Nakazawa and Shin-ya Katsumata. Extensional models of untyped lambda-mu calculus. In Herman Geuvers and Ugo de'Liguoro, editors, Proceedings Fourth Workshop on Classical Logic and Computation (CL&C 2012), volume 97 ofElectric Proceedings in Theoretical Computer Science, pages 35–47, October 2012.
  5. Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. Type checking and typability in domain-free lambda calculi. Theoretical Computer Science, 412(44):6193–6207, October 2011.
  6. Koji Nakazawa and Makoto Tatsuta. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, 153:21–37, April 2008.
  7. Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications (TLCA2007), volume 4583 of Lecture Notes in Computer Science, pages 336–350. Springer, 2007.
  8. Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications (TLCA2007), volume 4583 of Lecture Notes in Computer Science, pages 336–350. Springer, 2007.
  9. Koji Nakazawa and Makoto Tatsuta. Strong normalization proof with CPS-translation for second order classical natural deduction. The Journal of Symbolic Logic, 68(3):851–859, September 2003.
  10. Koji Nakazawa. Confluency and strong normalizability of call-by-value λμ-calculus. Theoretical Computer Science, 290:429–463, January 2003.

BACK

top