1 citations · 3 across the 12 of their papers we have counts for
4 papers · 1 filter
A Hierarchy of Supermartingales for -Regular Verification
Satoshi Kura, Hiroshi Unno
We propose new supermartingale-based certificates for verifying almost sure satisfaction of -regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexic…
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…
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Pedro H. Azevedo de Amorim, Satoshi Kura, Philip Saville
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise…
Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Satoshi Kura, Hiroshi Unno, Takeshi Tsukada
Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem. We present a new…