RustHorn: CHC-based verification for Rust programs Y Matsushita, T Tsukada, N Kobayashi ACM Transactions on Programming Languages and Systems (TOPLAS) 43 (4), 1-54, 2021 | 96 | 2021 |

Higher-order program verification via HFL model checking N Kobayashi, T Tsukada, K Watanabe Programming Languages and Systems: 27th European Symposium on Programming …, 2018 | 37 | 2018 |

Generalised species of rigid resource terms T Tsukada, K Asada, CHL Ong 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017 | 37 | 2017 |

Nondeterminism in game semantics via sheaves T Tsukada, CHL Ong 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 220-231, 2015 | 35 | 2015 |

A logical foundation for environment classifiers T Tsukada, A Igarashi Logical Methods in Computer Science 6, 2010 | 35 | 2010 |

Compositional higher-order model checking via *ω*-regular games over Böhm treesT Tsukada, CHL Ong Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference …, 2014 | 33 | 2014 |

Species, profunctors and taylor expansion weighted by SMCC: A unified framework for modelling nondeterministic, probabilistic and quantum programs T Tsukada, K Asada, CHL Ong Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 31 | 2018 |

Untyped recursion schemes and infinite intersection types T Tsukada, N Kobayashi International Conference on Foundations of Software Science and …, 2010 | 19 | 2010 |

Reduction from branching-time property verification of higher-order programs to HFL validity checking K Watanabe, T Tsukada, H Oshikawa, N Kobayashi Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and …, 2019 | 18 | 2019 |

Plays as resource terms via non-idempotent intersection types T Tsukada, CHL Ong Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer …, 2016 | 18 | 2016 |

Two-level game semantics, intersection types, and recursion schemes CHL Ong, T Tsukada International Colloquium on Automata, Languages, and Programming, 325-336, 2012 | 16 | 2012 |

Exact flow analysis by higher-order model checking Y Tobita, T Tsukada, N Kobayashi Functional and Logic Programming: 11th International Symposium, FLOPS 2012 …, 2012 | 15 | 2012 |

Innocent Strategies are Sheaves over Plays---Deterministic, Non-deterministic and Probabilistic Innocence T Tsukada, CHL Ong arXiv preprint arXiv:1409.2764, 2014 | 14 | 2014 |

Automated synthesis of functional programs with auxiliary functions S Eguchi, N Kobayashi, T Tsukada Programming Languages and Systems: 16th Asian Symposium, APLAS 2018 …, 2018 | 10 | 2018 |

A Truly Concurrent Game Model of the Asynchronous-Calculus K Sakayori, T Tsukada International Conference on Foundations of Software Science and Computation …, 2017 | 10 | 2017 |

Unsafe order-2 tree languages are context-sensitive N Kobayashi, K Inaba, T Tsukada Foundations of Software Science and Computation Structures: 17th …, 2014 | 10 | 2014 |

On computability of logical approaches to branching-time property verification of programs T Tsukada Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020 | 9 | 2020 |

Automatically disproving fair termination of higher-order functional programs K Watanabe, R Sato, T Tsukada, N Kobayashi ACM SIGPLAN Notices 51 (9), 243-255, 2016 | 9 | 2016 |

Complexity of model-checking call-by-value programs T Tsukada, N Kobayashi Foundations of Software Science and Computation Structures: 17th …, 2014 | 9 | 2014 |

Streett automata model checking of higher-order recursion schemes R Suzuki, K Fujima, N Kobayashi, T Tsukada 2nd International Conference on Formal Structures for Computation and …, 2017 | 8 | 2017 |