Keiko Nakata

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

Program committees

European projects

PhD Students

Master Students

Drafts

• Keiko Nakata
  Lazy mixins and disciplined effects. (.pdf) Lyre is the name of a train that took me home at Orsay from Paris. (By the way, Orsay is not Estonia.)
• Keiko Nakata
  Lazy Modules. (.pdf) I know Osan is not a beautiful name. It is taken from Soseki's novel "Wagahai wa Neko dearu (I Am a Cat)"; the novel which saved my stay in Paris.

Research papers

• Willard Rafnsson, Keiko Nakata, Andrei Sabelfeld
  Secure Class Initialization To appear in IEEE Transactions on Dependable and Secure Computing.
• Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin
  Classical call-by-need sequent calculi: The unity of semantic artifacts To appear in the 11th Int. Symp. on Functional and Logic Programming (FLOPS) 2012.
• Jacques Garrigue, Keiko Nakata.
  Path Resolution for Nested Recursive Modules. To appear in Higher-Order and Symbolic Computation. (.pdf [author])
• Marc Bezem, Keiko Nakata, Tarmo Uustalu
  On streams that are finitely red. Accepted for publication in Logical Methods in Computer Science.
• 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. To appear in the 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. To appear in 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