1 citations · 1 across the 1 of their papers we have counts for
5 papers
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
Kazuki Watanabe, Mayuko Kori, Taro Sekiyama +2
We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a…
Decision Tree Learning in CEGIS-Based Termination Analysis
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample G…
General Semantic Construction of Dependent Refinement Type Systems, Categorically
Satoshi Kura
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of…
Graded Algebraic Theories
Satoshi Kura
We provide graded extensions of algebraic theories and Lawvere theories that correspond to graded monads. We prove that graded algebraic theories, graded Lawvere theories, and fini…
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes…