arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · cs/0404055

Finite-Tree Analysis for Constraint Logic-Based Languages: The Complete Unabridged Version

Roberto Bagnara·Roberta Gori·Patricia M. Hill·Enea Zaffanella
View original source ↗Read source document ↗Export metadata ↓

Abstract

Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the safe omission of the occurs-check) and increased expressivity (cyclic terms can provide very efficient representations of grammars and other useful objects). Unfortunately, the use of infinite rational trees has problems. For instance, many of the built-in and library predicates are ill-defined for such trees and need to be supplemented by run-time checks whose cost may be significant. Moreover, some widely-used program analysis and manipulation techniques are correct only for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of the program variables (the finite variables) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new data-flow analysis, based on abstract interpretation, that captures such information.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Roberto Bagnara, Roberta Gori, Patricia M. Hill, Enea Zaffanella. 2004-04-27. Finite-Tree Analysis for Constraint Logic-Based Languages: The Complete Unabridged Version. https://arxiv.org/abs/cs/0404055

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Physically-Realisable Quantum Programming Language with Quantum-Controlled Quantum Channels

In contrast to a classical bit, which can only take the value $0$ or $1$, its quantum counterpart---a qubit---can exist in a superposition of $0$ and $1$. This is a superposition of data values, and it is then tempting to superpose programs as well. Indeed, a particular superposition of programs, known as the quantum SWITCH, has attracted considerable attention. A natural way to superpose programs is conditional branching on quantum data, and several studies have pursued this idea. However, there is a well-known semantic difficulty with this approach, and the fundamental question of whether the languages proposed in prior work can be physically realised remains open. This paper proposes a physically realisable quantum programming language with quantum branching over quantum channels. We first analyse the semantic difficulty from an implementation perspective and show that the difficulty is caused by arbitrariness in the implementation. We then design a language that is free from this arbitrariness. As expected from its implementation-oriented design, our language is physically realisable. We argue for this from two directions: first, we give a method for compiling programs into quantum circuits; and second, we show that our programs stay within the physically admissible range, namely, that they neither yield probabilities greater than one nor violate causal inequalities. The absence of such violations is established through the inclusion of our language in QC-QC, a notion of realisability studied in physics.

cs.PL↗
arXiv2026

Nothing Is Shared Until You Synchronise: Reinterpreting Java for Data-Race Freedom

In mainstream shared-memory languages, programmers use synchronisation mechanisms such as locks to isolate shared data accesses across threads to avoid data races. Yet synchronisation enforces only a temporal ordering, while shared memory still communicates updates between threads at every ordinary read and write. To achieve isolation, programmers therefore need to understand the connection between ordering and communication, and to apply synchronisation correctly and consistently, while compilers and hardware optimise assuming they have. When programmers synchronise incorrectly, they lose isolation, and the semantics of their programs change without notice. We propose Sync-as-Share, a memory model built on isolation and communication rather than on the ordering of accesses to shared memory. We start from thread isolation, where each thread reads and writes a private view of memory, and reinterpret programs' existing synchronisation actions to also communicate updates explicitly. As nothing is communicated outside synchronisation actions, data races become impossible by construction. Instead, conflicting updates are detected at synchronisation points. Viewing synchronisation as explicit communication exposes the design decisions of what should be communicated, to whom, and what counts as a conflict. We propose two communication topologies with different trade-offs. We instantiate Sync-as-Share for Java by making the synchronisation actions already defined by its memory model the only points at which threads communicate, so Java programs can adopt Sync-as-Share unmodified. We formalise this instantiation as version-controlled memory, in which synchronisation actions push and pull updates between private views, and mechanise it in Rocq. We show that Java programs that are correctly synchronised under the Java memory model behave identically under shared memory and Sync-as-Share.

cs.PL↗
arXiv2026

GUARDTs: Decentralized Access Control for Replicated Data Types

Replicated data types providing strong eventual consistency offer a principled foundation for developing decentralized software. Yet existing approaches to programming such data types leave access control unresolved: they either provide none at all, delegate it to a trusted coordinator, reintroducing the centralization they were designed to avoid, or tie it to specific data-type constructions, while typically assuming non-Byzantine replicas and static policies. We present GUARDTs: Guarded Unforgeable Algebraic Replicated Data Types, which embed fine-grained permissions directly into the application data model, operate without a central authority, support dynamic policy evolution, and tolerate Byzantine replicas. We formally prove that GUARDTs guarantee confidentiality, integrity, and availability and show empirically that their access control adds negligible overhead on top of the cost of Byzantine-resilient replication itself.

cs.PL↗