Keiko Nakata

Bio

I like mathematics, in particular topology and logic, and programming. I am interested to understand how groups of people decide and work together in professional settings and how structure influences on it.

I hold a PhD in theoretical computer science from RIMS, Kyoto University, supervised by Jacques Garrigue and Masahito Hasegawa. I did a post-doc in Gallium, Inria, supervised by Xavier Leroy. I worked as a tenured senior researcher in Tarmo Uustalu's group at Tallinn U. of Technology. As a short-term visitor, I participated in the special year on Univalent Foundations of Mathematics at the Institute for Advanced Study.

Since 2015, I have moved to industry to expand my horizon. These days I am interested in distributed computing, social psychology and cryptography.

Program committees

PPL 2011 (Japanese), SOS 2011, DSL 2011, FLOPS 2012, ML 2012, EXPRESS/SOS 2012, APLAS 2012, PPL 2013 (Japanese), TFP 2013, FLOPS 2014, ML 2014, Haskell Symposium 2014, PEPM 2015, PPL 2015 (Japanese), TLCA 2015, ICFP 2015, ESOP 2016, ITP 2017, TYPES 2017, IFL 2018, TYPES 2018, TYPES 2019, PEPM 2019, FSCD 2020, TyDe 2021, IFL 2021, TYPES 2021, PEPM 2022. ML 2022

Past European projects

• COST CA15123 (EUTypes) WG4 (Types for verification) chair, 2016 March - 2020 March
• COST IC1402 (ARVI) WG3 (Challenging domains) co-chair, 2014 December - 2016 April
• HATS 2009 March - 2013 February
• COST IC1201 (BETTY) 2012 October - 2014 October

Organization of Scientific meetings and conferences

• NII Shonan meeting on Static Analysis Meets Runtime Verification, 2015, co-organizer
• NII Shonan meeting on Coinduction for Computation Structures and Programming Languages, 2013, co-organizer
• 21st European Symposium on Programming, ESOP 2012, workshop chair

Other academic service

Selection Committee for John C. Reynolds Doctoral Dissertation Award 2016

Supervised Master Students

Elmo Todurov

Research papers

• Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk:
  Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor 21st Int. Symp. on Formal Methods, FM 2016.
• Marc Bezem, Thierry Coquand, Keiko Nakata and Erik Parmann
  Realizability at Work: Separating Two Constructive Notions of Finiteness. 22nd Int. Conf. on Types for Proofs and Programs, TYPES 2016.
• Richard Bubel, Crystal Chang Din, Reiner Hähnle and Keiko Nakata
  A Dynamic Logic with Traces and Coinduction. 24th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2015.
• Keiko Nakata and Tarmo Uustalu.
  A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. 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).
• 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.
• 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.
• Keiko Nakata and Andrei Sabelfeld.
  Securing Class Initialization. In Proc. 4th IFIP WG 11.11 International Conference on Trust Management (IFIPTM), 2010.
• 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.
• Keiko Nakata and Masahito Hasegawa
  Small-step and big-step semantics for call-by-need. Journal of Functional Programming.
• 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.
• Keiko Nakata and Jacques Garrigue.
  Path resolution for recursive nested modules is undecidable. Presented at the 9th International Workshop on Termination (WST), 2007
• Keiko Nakata and Jacques Garrigue.
  Recursive Modules for Programming. Presented at The ACM SIGPLAN International Conference on Functional Programming (ICFP), 2006. 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.
• Keiko Nakata
  Recursion for structured modules. Presented at JSSST Workshop on Programming an d Programming Languages, Gunma, Japan, March 2005.
• 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.

Tutorial

• Resumption-based big-step and small-step interpreters for While with interactive I/O. IFIP Working Conference on Domain-Specific Languages, DSL, 2011.

Talks

• Introducing namespaces into SQL result sets using nested structural types at Typelevel Summit Berlin, 2015