Keiko Nakata

If you have a problem sendign me Japanese emails, please check here.

Program committees

European projects

Other academic service

PhD Students

Finished Master Students

Research papers

• Keiko Nakata and Tarmo Uustalu.
  A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. To appear in Logical Methods in Computer Science. The accompanying Coq development: abyss.tgz.
• Danko Ilik and Keiko Nakata
  A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. 19th Conf. on Types for Proofs and Programs, TYPES 2013.
• Willard Rafnsson, Keiko Nakata, Andrei Sabelfeld
  Secure Class Initialization. IEEE Transactions on Dependable and Secure Computing, 10(1).
• Keiko Nakta and Andri Saar
  Compiling cooperative task management to continuations. International Conference on Fundamentals of Software Engineering (FSEN) 2013.
• Hyeonseung Im, Keiko Nakata and Sungwoo Park
  Contractive signatures with recursive types, type parameters, and abstract types. 40th International Colloquium on Automata, Languages, and Programming (ICALP) 2013.
• Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin
  Classical call-by-need sequent calculi: The unity of semantic artifacts 11th Int. Symp. on Functional and Logic Programming (FLOPS) 2012.
• Jacques Garrigue, Keiko Nakata.
  Path Resolution for Nested Recursive Modules. Higher-Order and Symbolic Computation, 24(3). (.pdf [author])
• Marc Bezem, Keiko Nakata, Tarmo Uustalu
  On streams that are finitely red. Logical Methods in Computer Science, 8(4:4).
• Keiko Nakata, Tarmo Uustalu, Marc Bezem
  A Proof Pearl with the Fan Theorem and Bar Induction: Walking through Infinite Trees with Mixed Induction and Coinduction. 7th Asian Symposium on Programming Languages and Systems (APLAS) 2011.
• Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park
  A Syntactic Type System for Recursive Modules. ACM International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH/OOPSLA) 2011.
• Keiko Nakata
  Denotational semantics for lazy initialization of letrec: black holes as exceptions rather than nontermination. In Proc. 7th Workshop on Fixed Points in Computer Science (FICS) 2010. (.pdf)
• Keiko Nakata and Tarmo Uustalu.
  Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction. In Proc. Structural Operational Semantics (SOS) 2010. The accompanying Coq development: sophie.tgz. Sophie, after Det syke barn. I like his women paintings.
• Keiko Nakata and Andrei Sabelfeld.
  Securing Class Initialization. In Proc. 4th IFIP WG 11.11 International Conference on Trust Management (IFIPTM), 2010. (.pdf)
• Keiko Nakata and Tarmo Uustalu.
  A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. In Proc. 19th European Symposium on Programming (ESOP), 2010. (.pdf) The accompanying Coq development: abyss.tgz. Abyss is the name of my computer at KABA, my lab during doctoral study. I like its semantics and the film.
• Keiko Nakata and Masahito Hasegawa
  Small-step and big-step semantics for call-by-need. Journal of Functional Programming. (.pdf)© Cambridge University Press. Extended version at ArXiv. (.pdf)
• Keiko Nakata and Tarmo Uustalu.
  Trace-based Coinductive Operational Semantics for While: Big-step and Small-step, Relational and Functional Styles. In Proc. Theorem Proving in Higher Order Logics (TPHOLs), 2009. (.pdf© Springer-Verlag) The accompanying Coq development: majas.tar.gz. Majas means "in the house" in Estonian.
• Keiko Nakata and Jacques Garrigue.
  Path resolution for recursive nested modules is undecidable. Presented at the 9th International Workshop on Termination (WST), 2007 (.pdf)
• Keiko Nakata and Jacques Garrigue.
  Recursive Modules for Programming. Presented at The ACM SIGPLAN International Conference on Functional Programming (ICFP), 2006. (.pdf) I am fond of Marguerite Gautier's life and value.
• Keiko Nakata and Jacques Garrigue.
  Recursive modules for programming (extended abstract). Presented at JSSST Works hop on Programming and Programming Languages, Ogoto, Japan, March 2006. (.pdf)
• Keiko Nakata
  Recursion for structured modules. Presented at JSSST Workshop on Programming an d Programming Languages, Gunma, Japan, March 2005. (.pdf)
• Keiko Nakata, Akira Ito, Jacques Garrigue.
  Recursive Object-Oriented Modules. Presented at the 12th International Work shop on Foundations of Object-Oriented Languages (FOOL), Long Beach, California, January 2005. (.pdf)

Tutorial

• Resumption-based big-step and small-step interpreters for While with interactive I/O. IFIP Working Conference on Domain-Specific Languages, DSL, 2011. (.pdf) The accompanying Haskell code: (.tgz).

Talks

• Walking through infinite trees with mixed induction and coinduction. (.pdf)
• Mixed induction-coinduction at work for Coq. (.pdf) The accompanying Coq development: (.v)

Useful links

Less useful notes

Teaching