Keiko Nakata

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

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.
• Jacques Garrigue and Keiko Nakata.
  Path Resolution for Nested Recursive Modules. (.pdf)

Research papers

• 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 under preparation. 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 both the 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)

Talks

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

Useful links

Less useful notes