A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911216080781312 |
|---|---|
| author | Watanabe, Kazuki Kori, Mayuko Sekiyama, Taro Kura, Satoshi Unno, Hiroshi |
| author_facet | Watanabe, Kazuki Kori, Mayuko Sekiyama, Taro Kura, Satoshi Unno, Hiroshi |
| contents | We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational product construction -- from linear-time safety verification of effectful higher-order programs to computation of weakest pre-conditions of product programs. This reduction enables us to apply existing algorithms for such well-studied computations of weakest pre-conditions, some of which are available as off-the-shelf solvers. We show the correctness of our denotational product construction by proving a preservation theorem under strong monad morphisms and an existence of suitable liftings along a fibration. We instantiate our framework with both probabilistic and angelic nondeterministic higher-order programs, and implement an automated solver for the probabilistic case based on the existing solver developed by Kura and Unno. To the best of our knowledge, this is the first automated verifier for linear-time temporal verification of probabilistic higher-order programs with recursion. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_11320 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs Watanabe, Kazuki Kori, Mayuko Sekiyama, Taro Kura, Satoshi Unno, Hiroshi Logic in Computer Science We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational product construction -- from linear-time safety verification of effectful higher-order programs to computation of weakest pre-conditions of product programs. This reduction enables us to apply existing algorithms for such well-studied computations of weakest pre-conditions, some of which are available as off-the-shelf solvers. We show the correctness of our denotational product construction by proving a preservation theorem under strong monad morphisms and an existence of suitable liftings along a fibration. We instantiate our framework with both probabilistic and angelic nondeterministic higher-order programs, and implement an automated solver for the probabilistic case based on the existing solver developed by Kura and Unno. To the best of our knowledge, this is the first automated verifier for linear-time temporal verification of probabilistic higher-order programs with recursion. |
| title | A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2510.11320 |