Keiko Nakata

26 papers A 3B 3Misc 1Journal 10Unranked 9
YearRankTypeTitle / Venue / Authors
2016 B conf
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor.
FM
Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge luis Sacchini, Hendrik Tews, Thomas Tuerk
2016 — conf
Realizability at Work: Separating Two Constructive Notions of Finiteness.
TYPES
Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann
2015 B conf
A Dynamic Logic with Traces and Coinduction.
TABLEAUX
Richard Bubel, Crystal Chang Din, Reiner Hähnle, Keiko Nakata
2015 J jnl
A Hoare logic for the coinductive trace-based big-step semantics of While.
Log. Methods Comput. Sci.
Keiko Nakata, Tarmo Uustalu
2015 J jnl
Static analysis meets runtime verification (NII Shonan Meeting 2015-5).
NII Shonan Meet. Rep.
Cyrille Artho, Einar Broch Johnsen, Martin Leucker, Keiko Nakata
2013 — conf
A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators.
TYPES
Danko Ilik, Keiko Nakata
2013 J jnl
Coinduction for Computation Structures and Programming Languages (NII Shonan Meeting 2013-11).
NII Shonan Meet. Rep.
Ichiro Hasuo, Keiko Nakata, Tarmo Uustalu
2013 — conf
Compiling Cooperative Task Management to Continuations.
FSEN
Keiko Nakata, Andri Saar
2013 — conf
Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types.
ICALP (2)
Hyeonseung Im, Keiko Nakata, Sungwoo Park
2013 J jnl
Securing Class Initialization in Java-like Languages.
IEEE Trans. Dependable Secur. Comput.
Willard Rafnsson, Keiko Nakata, Andrei Sabelfeld
2012 J jnl
A Constructive Proof of Open Induction Using Delimited Control Operators
CoRR
Danko Ilik, Keiko Nakata
2012 Misc conf
Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts.
FLOPS
Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin
2012 J jnl
On streams that are finitely red
Log. Methods Comput. Sci.
Marc Bezem, Keiko Nakata, Tarmo Uustalu
2011 B conf
A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction.
APLAS
Keiko Nakata, Tarmo Uustalu, Marc Bezem
2011 A conf
A syntactic type system for recursive modules.
OOPSLA
Hyeonseung Im, Keiko Nakata, Jacques Garrigue, Sungwoo Park
2011 J jnl
Path resolution for nested recursive modules.
High. Order Symb. Comput.
Jacques Garrigue, Keiko Nakata
2011 — conf
Resumption-based big-step and small-step interpreters for While with interactive I/O
DSL
Keiko Nakata
2010 A conf
A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While.
ESOP
Keiko Nakata, Tarmo Uustalu
2010 — conf
Denotational Semantics for Lazy Initialization of letrec.
FICS
Keiko Nakata
2010 — conf
Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
SOS
Keiko Nakata, Tarmo Uustalu
2010 — conf
Securing Class Initialization.
IFIPTM
Keiko Nakata, Andrei Sabelfeld
2009 J jnl
Lazy mixin modules and disciplined effects
CoRR
Keiko Nakata
2009 J jnl
Small-step and big-step semantics for call-by-need
CoRR
Keiko Nakata, Masahito Hasegawa
2009 J jnl
Small-step and big-step semantics for call-by-need.
J. Funct. Program.
Keiko Nakata, Masahito Hasegawa
2009 — conf
Trace-Based Coinductive Operational Semantics for While.
TPHOLs
Keiko Nakata, Tarmo Uustalu
2006 A conf
Recursive modules for programming.
ICFP
Keiko Nakata, Jacques Garrigue