Recursive modules for programming. - Keiko Nakata 001; Jacques Garrigue (ICFP, 2006)

Trace-Based Coinductive Operational Semantics for While. - Keiko Nakata 001; Tarmo Uustalu (TPHOLs, 2009)

Lazy mixin modules and disciplined effects - Keiko Nakata 001 (CoRR, 2009)

Small-step and big-step semantics for call-by-need. - Keiko Nakata 001; Masahito Hasegawa (J. Funct. Program., 2009)

Denotational Semantics for Lazy Initialization of letrec. - Keiko Nakata 001 (FICS, 2010)

Securing Class Initialization. - Keiko Nakata 001; Andrei Sabelfeld (IFIPTM, 2010)

Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction - Keiko Nakata 001; Tarmo Uustalu (SOS, 2010)

A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. - Keiko Nakata 001; Tarmo Uustalu; Marc Bezem (APLAS, 2011)

A syntactic type system for recursive modules. - Hyeonseung Im; Keiko Nakata 001; Jacques Garrigue; Sungwoo Park (OOPSLA, 2011)

Resumption-based big-step and small-step interpreters for While with interactive I/O - Keiko Nakata 001 (DSL, 2011)

Path resolution for nested recursive modules. - Jacques Garrigue; Keiko Nakata 001 (High. Order Symb. Comput., 2011)

Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. - Zena M. Ariola; Paul Downen; Hugo Herbelin; Keiko Nakata 001; Alexis Saurin (FLOPS, 2012)

A Constructive Proof of Open Induction Using Delimited Control Operators - Danko Ilik; Keiko Nakata 001 (CoRR, 2012)

On streams that are finitely red - Marc Bezem; Keiko Nakata 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2012)

Compiling Cooperative Task Management to Continuations. - Keiko Nakata 001; Andri Saar (FSEN, 2013)

Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types. - Hyeonseung Im; Keiko Nakata 001; Sungwoo Park (ICALP (2), 2013)

A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. - Danko Ilik; Keiko Nakata 001 (TYPES, 2013)

Coinduction for Computation Structures and Programming Languages (NII Shonan Meeting 2013-11). - Ichiro Hasuo; Keiko Nakata 001; Tarmo Uustalu (NII Shonan Meet. Rep., 2013)

Securing Class Initialization in Java-like Languages. - Willard Rafnsson; Keiko Nakata 001; Andrei Sabelfeld (IEEE Trans. Dependable Secur. Comput., 2013)

A Dynamic Logic with Traces and Coinduction. - Richard Bubel; Crystal Chang Din; Reiner Hähnle; Keiko Nakata 001 (TABLEAUX, 2015)

A Hoare logic for the coinductive trace-based big-step semantics of While. - Keiko Nakata 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2015)

Static analysis meets runtime verification (NII Shonan Meeting 2015-5). - Cyrille Artho; Einar Broch Johnsen; Martin Leucker; Keiko Nakata 001 (NII Shonan Meet. Rep., 2015)

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. - Hanno Becker; Juan Manuel Crespo; Jacek Galowicz; Ulrich Hensel; Yoichi Hirai; César Kunz; Keiko Nakata 001; Jorge Luis Sacchini; Hendrik Tews; Thomas Tuerk (FM, 2016)

Realizability at Work: Separating Two Constructive Notions of Finiteness. - Marc Bezem; Thierry Coquand; Keiko Nakata 001; Erik Parmann (TYPES, 2016)