Cover Image

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Watanabe, Kazuki, Kori, Mayuko, Sekiyama, Taro, Kura, Satoshi, Unno, Hiroshi
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
by: Kura, Satoshi, et al.
Published: (2024)

A Category-Theoretic Framework for Dependent Effect Systems
by: Kura, Satoshi, et al.
Published: (2026)

A Hierarchy of Supermartingales for $ω$-Regular Verification
by: Kura, Satoshi, et al.
Published: (2025)

A No-go Theorem for Coalgebraic Product Construction
by: Kori, Mayuko, et al.
Published: (2025)

From Coalgebraic Determinization to Belief Construction for Partial Observability
by: Kori, Mayuko, et al.
Published: (2026)

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
by: Kura, Satoshi, et al.
Published: (2025)

Higher-Order Weakest Precondition Transformers via a CPS Transformation
by: Kura, Satoshi
Published: (2023)

Initial Algebra Correspondence under Reachability Conditions
by: Kori, Mayuko, et al.
Published: (2025)

On Complete Categorical Semantics for Effect Handlers
by: Kura, Satoshi
Published: (2026)

Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC
by: Kori, Mayuko
Published: (2026)

Formal Verification of Probing Security via Conditional Independence
by: Kura, Satoshi, et al.
Published: (2026)

A Unifying Approach to Product Constructions for Quantitative Temporal Inference
by: Watanabe, Kazuki, et al.
Published: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
by: Goncharov, Sergey, et al.
Published: (2026)

Composing Codensity Bisimulations
by: Kori, Mayuko, et al.
Published: (2024)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

Denotational semantics driven simplicial homology?
by: Barbarossa, Davide
Published: (2024)

A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)
by: de Amorim, Pedro H. Azevedo, et al.
Published: (2026)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Compositional Verification of Almost-Sure Büchi Objectives in MDPs
by: van der Vegt, Marck, et al.
Published: (2025)

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games
by: Watanabe, Kazuki
Published: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Logical relations for call-by-push-value models, via internal fibrations in a 2-category
by: de Amorim, Pedro H. Azevedo, et al.
Published: (2025)

Denotational Foundations for Expected Cost Analysis
by: de Amorim, Pedro H. Azevedo
Published: (2024)

Wiring the Pi-calculus to Denotational Semantics
by: Sakayori, Ken, et al.
Published: (2026)

Expectation-based Analysis of Higher-Order Quantum Programs
by: Avanzini, Martin, et al.
Published: (2025)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Equilibrium Semantics and Strong Equivalence for Higher-Order Logic Programs
by: Charalambidis, Angelos, et al.
Published: (2026)

Syntactic Effectful Realizability in Higher-Order Logic
by: Cohen, Liron, et al.
Published: (2025)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
by: Chirica, Ion, et al.
Published: (2025)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
by: Goncharov, Sergey, et al.
Published: (2024)

Higher-Order Asynchronous Effects
by: Ahman, Danel, et al.
Published: (2023)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
by: Bacci, Giorgio, et al.
Published: (2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Craig Interpolation in Program Verification
by: Rümmer, Philipp
Published: (2026)

A Program Instrumentation Framework for Automatic Verification
by: Amilon, Jesper, et al.
Published: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, et al.
Published: (2025)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
by: Yang, Bowen, et al.
Published: (2026)

Hammering Higher Order Set Theory
by: Brown, Chad E., et al.
Published: (2025)