Cover Image

Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Endo, Ryunosuke, Terauchi, Tachio
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Hybrid Intersection Types for PCF (Extended Version)
by: Barenbaum, Pablo, et al.
Published: (2024)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
by: de Vilhena, Paulo Emílio, et al.
Published: (2021)

On Higher-Order Reachability Games vs May Reachability
by: Asada, Kazuyuki, et al.
Published: (2022)

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
by: Kobayashi, Naoki
Published: (2024)

PVASS Reachability is Decidable
by: Guttenberg, Roland, et al.
Published: (2025)

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
by: Deng, Haotian, et al.
Published: (2025)

Deciding Serializability in Network Systems
by: Amir, Guy, et al.
Published: (2026)

Decidable By Construction: Design-Time Verification for Trustworthy AI
by: Haynes, Houston
Published: (2026)

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

Strong Normalisation for Asynchronous Effects
by: Ahman, Danel, et al.
Published: (2026)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
by: Zilberstein, Noam, et al.
Published: (2023)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
by: Zilberstein, Noam
Published: (2024)

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

The Alternation Hierarchy of First-Order Logic on Words is Decidable
by: Barloy, Corentin, et al.
Published: (2025)

Finitary Truly Concurrent Bisimulations
by: Wang, Yong
Published: (2026)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

A coherent differential PCF
by: Ehrhard, Thomas
Published: (2022)

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

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

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

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
by: Kobayashi, Kentaro, et al.
Published: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

The Functional Machine Calculus III: Control
by: Heijltjes, Willem
Published: (2025)

Orthologic Type Systems
by: Guilloud, Simon, et al.
Published: (2025)

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
by: Rowicki, Radosław Jan, et al.
Published: (2025)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Proceedings Twelfth Workshop on Fixed Points in Computer Science
by: Saurin, Alexis
Published: (2025)

A Lazy, Concurrent Convertibility Checker
by: Courant, Nathanaëlle, et al.
Published: (2025)

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

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Constructive characterisations of the must-preorder for asynchrony
by: Bernardi, Giovanni, et al.
Published: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Extended Abstract: Mutable Objects with Several Implementations
by: Kaufmann, Matt, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
by: Teuber, Samuel, et al.
Published: (2025)

Intrinsically Correct Algorithms and Recursive Coalgebras
by: Alexandru, Cass, et al.
Published: (2025)