Keiko Nakata
Cited by
Cited by
Trace-based coinductive operational semantics for While: big-step and small-step, relational and functional styles
K Nakata, T Uustalu
International Conference on Theorem Proving in Higher Order Logics, 375-390, 2009
A Hoare logic for the coinductive trace-based big-step semantics of While
K Nakata, T Uustalu
Logical Methods in Computer Science 11, 2015
Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: An exercise in mixed induction-coinduction
K Nakata, T Uustalu
arXiv preprint arXiv:1008.2112, 2010
Small-step and big-step semantics for call-by-need
K Nakata, M Hasegawa
Journal of Functional Programming 19 (6), 699-722, 2009
Classical call-by-need sequent calculi: The unity of semantic artifacts
ZM Ariola, P Downen, H Herbelin, K Nakata, A Saurin
Functional and Logic Programming: 11th International Symposium, FLOPS 2012 …, 2012
Recursive modules for programming
K Nakata, J Garrigue
ACM SIGPLAN Notices 41 (9), 74-86, 2006
A proof pearl with the fan theorem and bar induction: Walking through infinite trees with mixed induction and coinduction
K Nakata, T Uustalu, M Bezem
Programming Languages and Systems: 9th Asian Symposium, APLAS 2011, Kenting …, 2011
A dynamic logic with traces and coinduction
R Bubel, CC Din, R Hähnle, K Nakata
Automated Reasoning with Analytic Tableaux and Related Methods: 24th …, 2015
On streams that are finitely red
M Bezem, K Nakata, T Uustalu
Logical Methods in Computer Science 8, 2012
Contractive signatures with recursive types, type parameters, and abstract types
H Im, K Nakata, S Park
Automata, Languages, and Programming: 40th International Colloquium, ICALP …, 2013
A syntactic type system for recursive modules
H Im, K Nakata, J Garrigue, S Park
ACM SIGPLAN Notices 46 (10), 993-1012, 2011
Recursive object-oriented modules
K Nakata, A Ito, J Garrigue
Proc. FOOL 12, 2005
Securing class initialization in Java-like languages
W Rafnsson, K Nakata, A Sabelfeld
IEEE Transactions on Dependable and Secure Computing 10 (1), 1-13, 2012
Mixed induction-coinduction at work for Coq
K Nakata, T Uustalu
2nd Workshop of Coq users, developers, and contributors (2010). http://www …, 2010
Securing class initialization
K Nakata, A Sabelfeld
IFIP International Conference on Trust Management, 48-62, 2010
Denotational semantics for lazy initialization of letrec: black holes as exceptions rather than divergence
K Nakata
7th workshop on fixed points in computer science, 2010
A direct version of Veldman’s proof of open induction on Cantor space via delimited control operators
D Ilik, K Nakata
Leibniz International Proceedings in Informatics (LIPIcs) 26, 188-201, 2014
Compiling cooperative task management to continuations
K Nakata, A Saar
Fundamentals of Software Engineering: 5th International Conference, FSEN …, 2013
Path resolution for nested recursive modules
J Garrigue, K Nakata
Higher-Order and Symbolic Computation 24, 207-237, 2011
A direct constructive proof of open induction on cantor space
D Ilik, K Nakata
Preprint, available at http://arxiv. org/abs/1209.2229, 2012
The system can't perform the operation now. Try again later.
Articles 1–20