Cover Image

Modeling Reachability Types with Logical Relations

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bao, Yuyan, Jia, Songlin, Wei, Guannan, Bračevac, Oliver, Rompf, Tiark
Format:	Preprint
Published:	2023
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
by: Jia, Songlin, et al.
Published: (2024)

When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
by: He, Siyuan, et al.
Published: (2025)

Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer
by: Deng, Haotian, et al.
Published: (2025)

Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness
by: Bao, Yuyan, et al.
Published: (2025)

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

Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
by: He, Siyuan, et al.
Published: (2026)

Typestate via Revocable Capabilities
by: Jia, Songlin, et al.
Published: (2025)

What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version)
by: Xu, Yichen, et al.
Published: (2025)

Towards Definitional Interpreters for Hoare Logics
by: Sun, Ke, et al.
Published: (2026)

Logical Relations for Session-Typed Concurrency
by: Balzer, Stephanie, et al.
Published: (2023)

Tracking Capabilities for Safer Agents
by: Odersky, Martin, et al.
Published: (2026)

LACUNA: Safe Agents as Recursive Program Holes
by: Zhao, Yaoyu, et al.
Published: (2026)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

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

Tail Modulo Cons, OCaml, and Relational Separation Logic
by: Allain, Clément, et al.
Published: (2024)

A Monadic Implementation of Functional Logic Programs
by: Hanus, Michael, et al.
Published: (2026)

On Computational Indistinguishability and Logical Relations
by: Lago, Ugo Dal, et al.
Published: (2024)

Logic Programming with Extensible Types
by: Perez, Ivan, et al.
Published: (2026)

A Language-Agnostic Logical Relation for Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version)
by: Yao, Yue, et al.
Published: (2024)

A Modular Program-Transformation Framework for Reducing Specifications to Reachability
by: Beyer, Dirk, et al.
Published: (2025)

Pathological Cases for a Class of Reachability-Based Garbage Collectors
by: Sotoudeh, Matthew
Published: (2025)

Optimization of the Context-Free Language Reachability Matrix-Based Algorithm
by: Muravev, Ilia
Published: (2024)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

A Relational Solver for Constraint-based Type Inference
by: Domoratskiy, Eridan, et al.
Published: (2024)

Typing Requirement Model as Coroutines
by: Gu, Qiqi, et al.
Published: (2024)

From Program Logics to Language Logics
by: Cimini, Matteo
Published: (2024)

Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
by: Tanaka, Izumi, et al.
Published: (2026)

Typing Composable Coroutines
by: Gu, Qiqi, et al.
Published: (2023)

typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell
by: Kudasov, Nikolai, et al.
Published: (2024)

AlloyInEcore: Embedding of First-Order Relational Logic into Meta-Object Facility for Automated Model Reasoning
by: Erata, Ferhat, et al.
Published: (2024)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

Designing Walrus: Relational Programming with Rich Types, On-Demand Laziness, and Structured Traces
by: Cuéllar, Santiago, et al.
Published: (2025)

Representing Molecules with Algebraic Data Types: Beyond SMILES and SELFIES
by: Goldstein, Oliver, et al.
Published: (2025)

Types for Grassroots Logic Programs
by: Shapiro, Ehud
Published: (2026)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
by: Foo, Darius, et al.
Published: (2023)

A Note on Dynamic Bidirected Dyck-Reachability with Cycles
by: Zhang, Qirun
Published: (2024)

Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
by: Endo, Ryunosuke, et al.
Published: (2025)

Context-Aware Separation Logic
by: Meyer, Roland, et al.
Published: (2023)

Functional Logic Program Transformations
by: Hanus, Michael, et al.
Published: (2026)