Naoki Kobayashi

Generating author description...

All published works

Action	Title	Year	Authors
+ PDF Chat	On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus	2024	Naoki Kobayashi
+	Ownership Types for Verification of Programs with Pointer Arithmetic	2024	Izumi Tanaka Ken Sakayori Naoki Kobayashi
+	Borrowable Fractional Ownership Types for Verification	2023	Takashi Nakayama Yusuke Matsushita Ken Sakayori Ryosuke Sato Naoki Kobayashi
+	Ownership Types for Verification of Programs with Pointer Arithmetic	2023	Izumi Tanaka Ken Sakayori Naoki Kobayashi
+	Automatic HFL(Z) Validity Checking for Program Verification	2022	Kento Tanahashi Naoki Kobayashi Ryosuke Sato
+	On Higher-Order Reachability Games vs May Reachability	2022	Kazuyuki Asada Hiroyuki Katsura Naoki Kobayashi
+ PDF Chat	On Higher-Order Reachability Games Vs May Reachability	2022	Kazuyuki Asada Hiroyuki Katsura Naoki Kobayashi
+	Gradual Tensor Shape Checking	2022	Momoko Hattori Naoki Kobayashi Ryosuke Sato
+	A Simple and Strong Baseline for End-to-End Neural RST-style Discourse Parsing	2022	Naoki Kobayashi Tsutomu Hirao Hidetaka Kamigaito Manabu Okumura Masaaki Nagata
+	A Simple and Strong Baseline for End-to-End Neural RST-style Discourse Parsing	2022	Naoki Kobayashi Tsutomu Hirao Hidetaka Kamigaito Manabu Okumura Masaaki Nagata
+ PDF Chat	A Probabilistic Higher-order Fixpoint Logic	2021	Yo Mitani Naoki Kobayashi Takeshi Tsukada
+ PDF Chat	An Overview of the HFL Model Checking Project	2021	Naoki Kobayashi
+	Symbolic Automatic Relations and Their Applications to SMT and CHC Solving	2021	Takumi Shimoda Naoki Kobayashi Ken Sakayori Ryosuke Sato
+	Toward Neural-Network-Guided Program Synthesis and Verification	2021	Naoki Kobayashi Taro Sekiyama Issei Sato Hiroshi Unno
+	Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes	2021	Patrick Baillot Alexis Ghyselen Naoki Kobayashi
+	Symbolic Automatic Relations and Their Applications to SMT and CHC Solving	2021	Takumi Shimoda Naoki Kobayashi Ken Sakayori Ryosuke Sato
+	Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination	2021	Tsubasa Shoshi Takuma Ishikawa Naoki Kobayashi Ken Sakayori Ryosuke Sato Takeshi Tsukada
+ PDF Chat	Symbolic Automatic Relations and Their Applications to SMT and CHC Solving	2021	Takumi Shimoda Naoki Kobayashi Ken Sakayori Ryosuke Sato
+ PDF Chat	Toward Neural-Network-Guided Program Synthesis and Verification	2021	Naoki Kobayashi Taro Sekiyama Issei Sato Hiroshi Unno
+ PDF Chat	Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination	2021	Tsubasa Shoshi Takuma Ishikawa Naoki Kobayashi Ken Sakayori Ryosuke Sato Takeshi Tsukada
+	A Probabilistic Higher-order Fixpoint Logic.	2020	Yo Mitani Naoki Kobayashi Takeshi Tsukada
+ PDF Chat	Grammar Compression with Probabilistic Context-Free Grammar	2020	Hiroaki Naganuma Diptarama Hendrian Ryo Yoshinaka Ayumi Shinohara Naoki Kobayashi
+	ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs	2020	John Toman Ren Siqi Kohei Suenaga Atsushi Igarashi Naoki Kobayashi
+	Grammar compression with probabilistic context-free grammar	2020	Hiroaki Naganuma Diptarama Hendrian Ryo Yoshinaka Ayumi Shinohara Naoki Kobayashi
+	A Cyclic Proof System for HFLN	2020	Mayuko Kori Takeshi Tsukada Naoki Kobayashi
+	RustHorn: CHC-Based Verification for Rust Programs	2020	Yusuke Matsushita Takeshi Tsukada Naoki Kobayashi
+ PDF Chat	On the Termination Problem for Probabilistic Higher-Order Recursive Programs	2019	Naoki Kobayashi Ugo Dal Lago Charles Grellois
+	A Type-Based HFL Model Checking Algorithm	2019	Youkichi Hosoi Naoki Kobayashi Takeshi Tsukada
+ PDF Chat	A Type-Based HFL Model Checking Algorithm	2019	Youkichi Hosoi Naoki Kobayashi Takeshi Tsukada
+	Dust Coagulation Regulated by Turbulent Clustering in Protoplanetary Disks	2018	Takashi Ishihara Naoki Kobayashi Kei Enohata Masayuki Umemura Kenji Shiraishi
+	Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence	2018	Kazuyuki Asada Naoki Kobayashi Ryoma Sin’ya Takeshi Tsukada
+	Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence	2018	Kazuyuki Asada Naoki Kobayashi Ryoma Sin’ya Takeshi Tsukada
+	Pumping Lemma for Higher-order Languages	2017	Kazuyuki Asada Naoki Kobayashi
+	Proceedings Eighth Workshop on Intersection Types and Related Systems	2017	Naoki Kobayashi
+	Proceedings Eighth Workshop on Intersection Types and Related Systems	2017	Naoki Kobayashi
+	Pumping Lemma for Higher-order Languages	2017	Kazuyuki Asada Naoki Kobayashi
+	Higher-Order Program Verification via HFL Model Checking	2017	Naoki Kobayashi Takeshi Tsukada Keiichi Watanabe
+ PDF Chat	Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence	2017	Ryoma Sin’ya Kazuyuki Asada Naoki Kobayashi Takeshi Tsukada
+	On Word and Frontier Languages of Unsafe Higher-Order Grammars	2016	Kazuyuki Asada Naoki Kobayashi
+ PDF Chat	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus	2012	Naoki Kobayashi C.-H. Luke Ong
+ PDF Chat	Hybrid Schemes of Shock Capturing Methods and Secondary Conservative Finite Difference	2011	Yohei MORINISHI Naoki Kobayashi Kazuki Koga
+ PDF Chat	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus	2009	Naoki Kobayashi C.-H. Luke Ong
+	Maximum distributions of noncolliding Bessel bridges	2008	Naoki Kobayashi Minami Izumi Makoto Katori
+	Large Qudit Limit of One-dimensional Quantum Walks	2008	Mitsunori Sato Naoki Kobayashi Makoto Katori Norio Konno
+ PDF Chat	Resource Usage Analysis for the Pi-Calculus	2006	Naoki Kobayashi Kohei Suenaga Lucian Wischik

Common Coauthors

Coauthor	Papers Together
Takeshi Tsukada	12
Ryosuke Sato	8
Kazuyuki Asada	8
Ken Sakayori	8
Ryoma Sin’ya	3
Takumi Shimoda	3
Makoto Katori	2
Youkichi Hosoi	2
Hidetaka Kamigaito	2
Taro Sekiyama	2
C.-H. Luke Ong	2
Yusuke Matsushita	2
Hiroyuki Katsura	2
Manabu Okumura	2
Hiroshi Unno	2
Tsubasa Shoshi	2
Diptarama Hendrian	2
Issei Sato	2
Yo Mitani	2
Kohei Suenaga	2
Ayumi Shinohara	2
Hiroaki Naganuma	2
Ryo Yoshinaka	2
Masaaki Nagata	2
Izumi Tanaka	2
Takuma Ishikawa	2
Tsutomu Hirao	2
John Toman	1
Mayuko Kori	1
Mitsunori Sato	1
Minami Izumi	1
Lucian Wischik	1
Alexis Ghyselen	1
Keiichi Watanabe	1
Kazuki Koga	1
Charles Grellois	1
Atsushi Igarashi	1
Kenji Shiraishi	1
Takashi Nakayama	1
Ren Siqi	1
Momoko Hattori	1
Ugo Dal Lago	1
Masayuki Umemura	1
Takashi Ishihara	1
Yohei MORINISHI	1
Patrick Baillot	1
Kento Tanahashi	1
Norio Konno	1
Kei Enohata	1

Commonly Cited References

Action	Title	Year	Authors	# of times referenced
+ PDF Chat	SMT-based model checking for recursive programs	2016	Anvesh Komuravelli Arie Gurfinkel Sagar Chaki	9
+ PDF Chat	The Complexity of Model Checking Higher-Order Fixpoint Logic	2007	Roland Axelsson Martin Lange Rafał Somla	5
+ PDF Chat	Horn-ICE learning for synthesizing invariants and contracts	2018	P. Ezudheen Daniel Neider Deepak D’Souza Pranav Garg P. Madhusudan	5
+ PDF Chat	A Type-Directed Negation Elimination	2015	Étienne Lozes	5
+ PDF Chat	Refinement Type Inference via Horn Constraint Optimization	2015	Kodai Hashimoto Hiroshi Unno	4
+	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates	2020	Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi Maurizio Proietti	3
+ PDF Chat	Solving Horn Clauses on Inductive Data Types Without Induction	2018	Emanuele De Angelis Fabio Fioravanti Alberto Pettorossi Maurizio Proietti	3
+ PDF Chat	Work Analysis with Resource-Aware Session Types	2018	Ankush Das Jan Hoffmann Frank Pfenning	3
+ PDF Chat	On the Termination Problem for Probabilistic Higher-Order Recursive Programs	2019	Naoki Kobayashi Ugo Dal Lago Charles Grellois	3
+ PDF Chat	Parallel complexity analysis with temporal session types	2018	Ankush Das Jan Hoffmann Frank Pfenning	3
+	Model-checking process equivalences	2014	Martin Lange Étienne Lozes Manuel Vargas	3
+ PDF Chat	Automating Induction for Solving Horn Clauses	2017	Hiroshi Unno Sho Torii Hiroki Sakamoto	2
+ PDF Chat	Linearly Refined Session Types	2012	Pedro Baltazar Dimitris Mostrous Vasco T. Vasconcelos	2
+ PDF Chat	Verifying Properties of Binarized Deep Neural Networks	2018	Nina Narodytska Shiva Prasad Kasiviswanathan Leonid Ryzhyk Mooly Sagiv Toby Walsh	2
+ PDF Chat	Data flow refinement type inference	2021	Zvonimir Pavlinovic Yusen Su Thomas Wies	2
+	Learning nonlinear loop invariants with gated continuous logic networks	2020	Jianan Yao Gabriel Ryan Justin Wong Suman Jana Ronghui Gu	2
+	An inductive synthesis framework for verifiable reinforcement learning	2019	He Zhu Zikang Xiong S. Magill Suresh Jagannathan	2
+	Adam: A Method for Stochastic Optimization	2014	Diederik P. Kingma Jimmy Ba	2
+ PDF Chat	Asymptotically almost all \lambda-terms are strongly normalizing	2013	René David Katarzyna Grygiel Jakub Kozik Christophe Raffalli Guillaume Theyssier Marek Zaionc	2
+ PDF Chat	A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata	2007	Klaus Aehlig	2
+ PDF Chat	Learning Safe Neural Network Controllers with Barrier Certificates	2020	Hengjun Zhao Xia Zeng Taolue Chen Zhiming Liu Jim Woodcock	2
+ PDF Chat	Counting and generating lambda terms	2013	Katarzyna Grygiel Pierre Lescanne	2
+ PDF Chat	Safety Verification of Deep Neural Networks	2017	Xiaowei Huang Marta Kwiatkowska Sen Wang Min Wu	2
+ PDF Chat	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus	2009	Naoki Kobayashi C.-H. Luke Ong	2
+	Automatic structures	2002	Achim Blumensath Erich Grädel	2
+ PDF Chat	Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks	2017	Guy Katz Clark Barrett David L. Dill Kyle D. Julian Mykel J. Kochenderfer	2
+ PDF Chat	A Type-Based HFL Model Checking Algorithm	2019	Youkichi Hosoi Naoki Kobayashi Takeshi Tsukada	2
+ PDF Chat	Faster Fully Compressed Pattern Matching by Recompression	2015	Artur Jeż	1
+ PDF Chat	A simple model for the evolution of the dust population in protoplanetary disks	2012	T. Birnstiel Hubert Klahr Barbara Ercolano	1
+ PDF Chat	Łukasiewicz mu-Calculus	2013	Matteo Mio Alex Simpson	1
+ PDF Chat	Efficient Implementation of Weighted ENO Schemes	1996	Guang-Shan Jiang Chi‐Wang Shu	1
+	Analytic Combinatorics	2009	Philippe Flajolet Robert Sedgewick	1
+ PDF Chat	On the Hardness of Almost–Sure Termination	2015	Benjamin Lucien Kaminski Joost-Pieter Katoen	1
+ PDF Chat	On coinductive equivalences for higher-order probabilistic functional programs	2014	Ugo Dal Lago Davide Sangiorgi Michele Alberti	1
+ PDF Chat	NUMERICAL MODELING OF THE COAGULATION AND POROSITY EVOLUTION OF DUST AGGREGATES	2009	Satoshi Okuzumi Hidekazu Tanaka M. Sakagami	1
+ PDF Chat	Turbulence-induced collisional velocities and density enhancements: large inertial range results from shell models	2012	Alexander Hubbard	1
+ PDF Chat	A survey of several finite difference methods for systems of nonlinear hyperbolic conservation laws	1978	Gary A. Sod	1
+ PDF Chat	TURBULENCE-INDUCED RELATIVE VELOCITY OF DUST PARTICLES. I. IDENTICAL PARTICLES	2013	Liubin Pan Paolo Padoan	1
+	Proceedings Sixth Workshop on Intersection Types and Related Systems	2013	Stéphane Graham-Lengrand Luca Paolini	1
+	Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types	2013	Nikolaj Bjørner Kenneth L. McMillan Andrey Rybalchenko	1
+	Representation Theory: A First Course	1991	William Fulton	1
+	A New Approach to Probabilistic Programming Inference	2014	Frank Wood Jan-Willem van de Meent Vikash K. Mansinghka	1
+ PDF Chat	Fully Online Grammar Compression in Constant Space	2014	Shirou Maruyama Yasuo Tabei	1
+	Towards the ultimate conservative difference scheme. V. A second-order sequel to Godunov's method	1979	Bram van Leer	1
+ PDF Chat	Tree Structure Compression with RePair	2011	Markus Lohrey Sebastian Maneth Roy Mennicke	1
+ PDF Chat	Better Document-level Sentiment Analysis from RST Discourse Parsing	2015	Parminder Bhatia Yangfeng Ji Jacob Eisenstein	1
+ PDF Chat	Bouncing behavior of microscopic dust aggregates	2013	A. Seizinger W. Kley	1
+	Comparison of finite volume flux vector splittings for the Euler equations	1986	W. Kyle Anderson James L. Thomas Bram van Leer	1
+ PDF Chat	A high-wavenumber viscosity for high-resolution numerical methods	2003	Andrew W. Cook W. Cabot	1
+ PDF Chat	Finitary Semantics of Linear Logic and Higher-Order Model-Checking	2015	Charles Grellois Paul-André Melliès	1