29 citations · 78 across the 14 of their papers we have counts for
5 papers · 1 filter
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…
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…
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…