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

• 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)
• 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)
• 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)
• 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.