| 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 | 61 | 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 | 51 | 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 | 46 | 2010 |
| Small-step and big-step semantics for call-by-need K Nakata, M Hasegawa Journal of Functional Programming 19 (6), 699-722, 2009 | 35 | 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 | 32 | 2012 |
| Recursive modules for programming K Nakata, J Garrigue ACM SIGPLAN Notices 41 (9), 74-86, 2006 | 31 | 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 | 24 | 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 | 17 | 2015 |
| On streams that are finitely red M Bezem, K Nakata, T Uustalu Logical Methods in Computer Science 8, 2012 | 15 | 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 | 11 | 2013 |
| A syntactic type system for recursive modules H Im, K Nakata, J Garrigue, S Park ACM SIGPLAN Notices 46 (10), 993-1012, 2011 | 10 | 2011 |
| Recursive object-oriented modules K Nakata, A Ito, J Garrigue Proc. FOOL 12, 2005 | 10 | 2005 |
| Mixed induction-coinduction at work for Coq K Nakata, T Uustalu 2nd Workshop of Coq users, developers, and contributors (2010). http://www …, 2010 | 7 | 2010 |
| 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 | 6 | 2012 |
| Securing class initialization K Nakata, A Sabelfeld IFIP International Conference on Trust Management, 48-62, 2010 | 6 | 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 | 6 | 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 | 5 | 2014 |
| Compiling cooperative task management to continuations K Nakata, A Saar Fundamentals of Software Engineering: 5th International Conference, FSEN …, 2013 | 5 | 2013 |
| Path resolution for nested recursive modules J Garrigue, K Nakata Higher-Order and Symbolic Computation 24, 207-237, 2011 | 4 | 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 | 3 | 2012 |
Tarmo UustaluProfessor, Reykjavik University / Lead research scientist, Tallinn University of TechnologyVerified email at ru.is
