29 citations · 78 across the 14 of their papers we have counts for
14 papers
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
Takeshi Tsukada, Kazuyuki Asada
A number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are "matrices" over appropriate coefficient sets. Examples include…
Automatic HFL(Z) Validity Checking for Program Verification
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato +1
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reducti…
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada, Hiroshi Unno
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our us…
Termination Analysis for the -Calculus by Reduction to Sequential Program Termination
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi +3
We propose an automated method for proving termination of -calculus processes, based on a reduction to termination of sequential programs: we translate a -calculus process to…
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Minchao Wu, Takeshi Tsukada, Hiroshi Unno +2
Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Desp…
A Probabilistic Higher-order Fixpoint Logic
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL an…
A Cyclic Proof System for HFLN
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with…
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two g…
RustHorn: CHC-based Verification for Rust Programs (full version)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointe…
A Type-Based HFL Model Checking Algorithm
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown th…
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence
Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya +1
It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-t…
Higher-Order Program Verification via HFL Model Checking
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher…
Innocent Strategies are Sheaves over Plays---Deterministic, Non-deterministic and Probabilistic Innocence
Takeshi Tsukada, C. -H. Luke Ong
Although the HO/N games are fully abstract for PCF, the traditional notion of innocence (which underpins these games) is not satisfactory for such language features as non-determin…
A Logical Foundation for Environment Classifiers
Takeshi Tsukada, Atsushi Igarashi
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragme…