Complete the Cycle: Reachability Types with Expressive Cyclic References

• URL: http://arxiv.org/abs/2503.07328v1
• Date: Mon, 10 Mar 2025 13:42:02 GMT
• Title: Complete the Cycle: Reachability Types with Expressive Cyclic References
• Authors: Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf,
• Abstract summary: Reachability Types (RT) are a qualified type system for tracking aliasing and separation in functional and higher-order programming.<n>Previous RT systems have been based on calculi that restrict cyclic dependencies and are shown to be terminating.<n>We extend RT with an expressive cyclic reference type that permits the formation of cyclic dependencies through the store.
• Score: 6.994376737187498
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Reachability Types (RT) are a qualified type system for tracking aliasing and separation in functional and higher-order programming. By formalizing resource reachability with a sound static type system, RT enable higher-order programming patterns with runtime safety and non-interference guarantees. However, previous RT systems have been based on calculi that restrict cyclic dependencies and are shown to be terminating in the absence of built-in recursive constructs. While termination is sometimes a desirable property, simplifying reasoning and ensuring predictable behavior, it implies an inability to encode expressive programs involving non-termination and advanced recursive patterns, such as mutual recursion and various fixed-point combinators. In this paper, we address this limitation by extending RT with an expressive cyclic reference type that permits the formation of cyclic dependencies through the store, thereby allowing the system to encode recursive programming patterns without relying on extra built-in constructs. In addition, we redesign qualifier typing in the reference introduction rule, allowing separate references to point to a shared and tracked referent. We formalize the system as the $\lambda^{\circ}_{<:}$-calculus, with a mechanized soundness proof via the standard progress and preservation lemmas. As a demonstration, we implement a well-typed fixpoint operator, proving that recursive patterns can be encoded using the novel cyclic reference type.

Related papers

• Triangulation as an Acceptance Rule for Multilingual Mechanistic Interpretability [0.0]
  We argue that mechanistic explanations for such models should satisfy a emphcausal standard.<n>Claims must survive causal interventions and must emphcross-reference across environments that perturb surface form while preserving meaning.<n>We ground triangulation in causal abstraction by casting it as an approximate transformation score over a distribution of interchange interventions, connect it to the pragmatic interpretability agenda, and present a comparative experimental protocol across model families, language pairs, and tasks.
  arXiv  Detail & Related papers  (2025-12-31T13:03:34Z)
• Robust Scene Coordinate Regression via Geometrically-Consistent Global Descriptors [52.57327385675752]
  We propose an aggregator module that learns global descriptors consistent with both geometrical structure and visual similarity.<n>This corrects erroneous associations caused by unreliable overlap scores.<n>Experiments on challenging benchmarks show substantial localization gains in large-scale environments.
  arXiv  Detail & Related papers  (2025-12-19T04:24:03Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• LIHE: Linguistic Instance-Split Hyperbolic-Euclidean Framework for Generalized Weakly-Supervised Referring Expression Comprehension [42.52759428579815]
  Existing Weakly-Supervised Referring Expression (WREC) methods are fundamentally limited by a one-to-one mapping assumption.<n>We introduce the Weakly-Supervised Generalized Referring Expression task (WGREC), a more practical paradigm that handles expressions with variable numbers of referents.<n>We propose a novel WGREC framework named Linguistic Instance-Split-Euclidean (LIHE), which operates in two stages.
  arXiv  Detail & Related papers  (2025-11-15T04:06:57Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDul is a language that unifies input transformations and predicate definitions into a single combined abstraction.<n>We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.
  arXiv  Detail & Related papers  (2025-11-13T18:06:21Z)
• Higher-order Linear Attention [59.92962330635185]
  quadratic cost of scaled dot-product attention is a central obstacle to scaling autoregressive language models to long contexts.<n>We introduce Higher-order Linear Attention (HLA), a causal, streaming mechanism that realizes higher interactions via compact prefix sufficient statistics.
  arXiv  Detail & Related papers  (2025-10-31T07:54:37Z)
• Selmer-Inspired Elliptic Curve Generation [0.0]
  Elliptic curve cryptography (ECC) is foundational to modern secure communication.<n>Existing standard curves have faced scrutiny for opaque parameter-generation practices.<n>This work introduces a Selmer-inspired framework for constructing elliptic curves that is both transparent and auditable.
  arXiv  Detail & Related papers  (2025-09-30T17:33:36Z)
• SIM-CoT: Supervised Implicit Chain-of-Thought [108.30049193668083]
  Implicit Chain-of-Thought (CoT) methods offer a token-efficient alternative to explicit CoT reasoning in Large Language Models.<n>We identify a core latent instability issue when scaling the computational budget of implicit CoT.<n>We propose SIM-CoT, a plug-and-play training module that introduces step-level supervision to stabilize and enrich the latent reasoning space.
  arXiv  Detail & Related papers  (2025-09-24T17:01:32Z)
• Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries [19.23701821549906]
  We propose a novel framework that combines symbolic execution, large language models (LLMs), and formal verification to generate Relatively Strongest Postconditions (RSPs)<n>Our approach leverages VST-A's symbolic execution to precisely track program execution paths and state transitions.<n>From generated RSPs, we automatically synthesize strongest non-redundant postconditions expressed within given domain specific language.
  arXiv  Detail & Related papers  (2025-06-11T09:33:02Z)
• Respecting Temporal-Causal Consistency: Entity-Event Knowledge Graphs for Retrieval-Augmented Generation [69.45495166424642]
  We develop a robust and discriminative QA benchmark to measure temporal, causal, and character consistency understanding in narrative documents.<n>We then introduce Entity-Event RAG (E2RAG), a dual-graph framework that keeps separate entity and event subgraphs linked by a bipartite mapping.<n>Across ChronoQA, our approach outperforms state-of-the-art unstructured and KG-based RAG baselines, with notable gains on causal and character consistency queries.
  arXiv  Detail & Related papers  (2025-06-06T10:07:21Z)
• Neuro-Symbolic Query Compiler [57.78201019000895]
  This paper presents QCompiler, a neuro-symbolic framework inspired by linguistic grammar rules and compiler design, to bridge this gap.<n>It theoretically designs a minimal yet sufficient Backus-Naur Form (BNF) grammar $G[q]$ to formalize complex queries.<n>The atomicity of the sub-queries in the leaf ensures more precise document retrieval and response generation, significantly improving the RAG system's ability to address complex queries.
  arXiv  Detail & Related papers  (2025-05-17T09:36:03Z)
• An Expressive Trace Logic for Recursive Programs [0.36832029288386137]
  We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics. Our results shed light on the correspondence between programming constructs and logical connectives.
  arXiv  Detail & Related papers  (2024-11-20T08:35:29Z)
• S-CFE: Simple Counterfactual Explanations [22.262567049579648]
  We tackle the problem of finding manifold-aligned counterfactual explanations for sparse data.<n>Our approach effectively produces sparse, manifold-aligned counterfactual explanations.
  arXiv  Detail & Related papers  (2024-10-21T07:42:43Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  Iterative refinement has emerged as an effective paradigm for enhancing the capabilities of large language models (LLMs) on complex tasks. We propose Context-Wise Order-Agnostic Language Modeling (COrAL) to overcome these challenges. Our approach models multiple token dependencies within manageable context windows, enabling the model to perform iterative refinement internally.
  arXiv  Detail & Related papers  (2024-10-12T23:56:19Z)
• Tractable Offline Learning of Regular Decision Processes [50.11277112628193]
  This work studies offline Reinforcement Learning (RL) in a class of non-Markovian environments called Regular Decision Processes (RDPs) Ins, the unknown dependency of future observations and rewards from the past interactions can be captured experimentally. Many algorithms first reconstruct this unknown dependency using automata learning techniques.
  arXiv  Detail & Related papers  (2024-09-04T14:26:58Z)
• Clap: a Semantic-Preserving Optimizing eDSL for Plonkish Proof Systems [7.469723382577489]
  Plonkish is a popular circuit format for developing zero-knowledge proof systems. We present Clap, the first Rust e agnostic with a proof system circuit format. Clap casts the problem of producing Plonkish systems and their witness generators as a semantic-preserving compilation problem.
  arXiv  Detail & Related papers  (2024-05-20T15:31:32Z)
• Spatial Semantic Recurrent Mining for Referring Image Segmentation [63.34997546393106]
  We propose Stextsuperscript2RM to achieve high-quality cross-modality fusion. It follows a working strategy of trilogy: distributing language feature, spatial semantic recurrent coparsing, and parsed-semantic balancing. Our proposed method performs favorably against other state-of-the-art algorithms.
  arXiv  Detail & Related papers  (2024-05-15T00:17:48Z)
• SymBa: Symbolic Backward Chaining for Structured Natural Language Reasoning [5.893124686141782]
  We propose a novel backward chaining system, which integrates a symbolic solver and an LLM.<n>In SymBa, the solver controls the proof process, and the LLM is only called when the solver requires new information to complete the proof.<n> Empowered by completeness, SymBa achieves a significant improvement in seven deductive, relational, and arithmetic reasoning benchmarks compared to the baselines.
  arXiv  Detail & Related papers  (2024-02-20T08:27:05Z)
• Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion [14.739369424331478]
  We introduce a general framework that nicely connects the abstract concepts of structural recursion in the programming language domain to sequence modeling problems and learned models' behavior. With our framework as a powerful conceptual tool, we identify different issues under various set-ups.
  arXiv  Detail & Related papers  (2024-01-23T18:07:38Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• Reference Twice: A Simple and Unified Baseline for Few-Shot Instance Segmentation [103.90033029330527]
  Few-Shot Instance (FSIS) requires detecting and segmenting novel classes with limited support examples. We introduce a unified framework, Reference Twice (RefT), to exploit the relationship between support and query features for FSIS.
  arXiv  Detail & Related papers  (2023-01-03T15:33:48Z)
• Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [59.125047512495456]
  We introduce a novel gated recurrent unit (GRU) with a weighted time-delay feedback mechanism. We show that $tau$-GRU can converge faster and generalize better than state-of-the-art recurrent units and gated recurrent architectures.
  arXiv  Detail & Related papers  (2022-12-01T02:26:34Z)
• Differentiable Inference of Temporal Logic Formulas [1.370633147306388]
  We demonstrate the first Recurrent Neural Network architecture for learning Signal Temporal Logic formulas. We present the first systematic comparison of formula inference methods.
  arXiv  Detail & Related papers  (2022-08-10T16:52:23Z)
• Temporally-Consistent Surface Reconstruction using Metrically-Consistent Atlases [131.50372468579067]
  We propose a method for unsupervised reconstruction of a temporally-consistent sequence of surfaces from a sequence of time-evolving point clouds. We represent the reconstructed surfaces as atlases computed by a neural network, which enables us to establish correspondences between frames. Our approach outperforms state-of-the-art ones on several challenging datasets.
  arXiv  Detail & Related papers  (2021-11-12T17:48:25Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  Two programs are equivalent if there exists a sequence of application of rewrite rules that leads to rewriting one program into the other. We propose a neural network architecture based on a transformer model to generate proofs of equivalence between program pairs. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.
  arXiv  Detail & Related papers  (2021-09-22T01:37:08Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jl is an extendable symbolic system which uses dynamic multiple dispatch to change behavior depending on the domain needs. We show that by formalizing a generic API on actions independent of implementation, we can retroactively add optimized data structures to our system. We demonstrate the ability to swap between classical term-rewriting simplifiers and e-graph-based term-rewriting simplifiers.
  arXiv  Detail & Related papers  (2021-05-09T14:22:43Z)
• Pattern-aware Data Augmentation for Query Rewriting in Voice Assistant Systems [10.332550622090718]
  We propose an augmentation framework that learns patterns from existing training pairs and generates rewrite candidates from rewrite labels inversely to compensate for insufficient QR training data. Our experimental results show its effectiveness compared with a fully trained QR baseline and demonstrate its potential application in boosting the QR performance on low-resource domains or locales.
  arXiv  Detail & Related papers  (2020-12-21T16:36:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.