arXiv subjects

Annette Bieniusa

Publications and source records attributed to Annette Bieniusa.

At least 19 recordsLinked to original sources

arXiv2026

A Datalog Framework for Conflict-Free Replicated Data Types

Distributed applications increasingly support local-first collaboration over shared data, allowing multiple users to perform updates concurrently without global coordination. Such collaboration requires careful design to capture the intended semantics of the concurrent interactions. We introduce a declarative framework for specifying and reasoning about the semantics of conflict-free replicated data types (CRDTs) and CRDT-based applications in Datalog. The framework models CRDT semantics as executable logic programs over operation contexts, making concurrency explicit and compositional, and thus amenable to automated analysis. As one application, we use property-based testing to compare implementations. To the best of our knowledge, this is the first work to systematically use Datalog as a foundation for prototyping and analyzing complex CRDTs and their compositions. We evaluate our methodology using a collaborative graph data editing case study and report experimentation results assessing correctness validation and scalability with an increasing number of operations and replicas.

cs.DC↗

arXiv2026

CobbleDB: Modelling Levelled Storage by Composition

We present a composition-based approach to building correctby-construction database backing stores. In previous work, we specified the behaviour of several store variants and proved their correctness and equivalence. Here, we derive a Java implementation: the simplicity of the specification makes manual construction straightforward. We leverage spec-guaranteed store equivalence to compose performance features, then demonstrate practical value with CobbleDB, a reimplementation of RocksDB's levelled storage.

cs.DB↗

arXiv2026

KI-Adventskalender: An Informal Learning Intervention for Data & AI Literacy

Secondary school students increasingly encounter AI systems whose outputs depend on data quality, evaluation choices and modeling assumptions. To provide accessible entry points to these interconnected concepts, we developed KI-Adventskalender, a free web-based extracurricular initiative with 24 didactically curated, short, guided micro-challenges released daily in December, targeting data-centric competencies and socio-technical themes that shape how data are interpreted in practice. Drawing on two annual iterations, we report aggregate platform traces characterizing participation and task-level engagement. Participation increased substantially in 2025, but early attrition persists. Progression stabilized after midpoint: among users reaching Day 12 in 2025, more than 75% completed the calendar. Competence cluster performance shifted across years; higher revision rates co-occurred with strong pass rates, suggesting sustained engagement. We use these observations to motivate a next-step measurement agenda: tighter task instrumentation, embedded micro-assessments and mixed-method evaluation designs that can distinguish persistence from conceptual uptake, knowledge progression and durable learning outcomes.

cs.HC↗

arXiv2026

Set-Theoretic Types for Erlang: Theory, Implementation, and Evaluation

Erlang's dynamic typing discipline can lead to runtime errors that persist even after process restarts. Some of these runtime errors could be prevented through static type checking. While Erlang provides a type specification language, the compiler does not enforce these types, thereby limiting their role to documentation purposes. Type checking Erlang code is challenging due to language features such as dynamic type tests, subtyping, equi-recursive types, polymorphism, intersection types in signatures, and untagged union types. This work presents a set-theoretic type system for Erlang which captures the core features of Erlang's existing type language. The formal type system guarantees type soundness, and ensures that type checking remains decidable. Additionally, an implementation of a type checker is provided, supporting all features of the Erlang type language and most term-level language constructs. A case study with modules from Erlang's standard library, an external project, and the type checker itself demonstrates its effectiveness in verifying real-world Erlang code.

cs.PL↗

arXiv2025

Semantic Subtyping for Maps in Erlang

In this paper we will construct a set-theoretic model of types featuring type variables, base types, set-theoretic types and map types. Syntax of map types spans all the map types available in Erlang. The model of types is used to define a semantic subtyping relation based on set containment. The novelty of this work is the definition of subtyping over parameteric map types.

cs.PL↗

arXiv2025

PRDTs: Composable Design and Verification of Consensus Protocols using Replicated Data Types

Consensus protocols are fundamental in distributed systems as they enable services with strong consistency properties. However, designing protocols optimized for specific use-cases under certain system assumptions is typically an error-prone process requiring expert knowledge. Furthermore, while most recent optimized protocols are variations of well-known algorithms like Paxos or Raft, they often necessitate complete re-implementations, potentially introducing new bugs and complicating the application of existing verification results. This approach impedes application-specific consistency protocols that can easily be amended or swapped out, depending on the given application and deployment scenario. We propose Protocol Replicated Data Types (PRDTs), a novel programming model for implementing consensus protocols using replicated data types (RDTs). Inspired by the knowledge-based view of consensus, PRDTs employ RDTs to monotonically accumulate knowledge until agreement is reached. This approach allows for implementations focusing on high-level protocol logic that abstracts away network details and facilitates automated verification. Moreover, by applying existing algebraic composition techniques for RDTs in the PRDT context, we enable composable protocol building-blocks for implementing complex protocols. We present a formal model of our approach and implement a proof procedure that allows automated reasoning about the consensus safety of concrete PRDT implementations. Additionally, we demonstrate the applicability of our model in verified PRDT-based implementations of existing consensus protocols, and report empirical performance evaluation results. Our findings indicate that the PRDT approach offers enhanced flexibility and composability in protocol design, facilitates reasoning about correctness, and is suited for real-world adoption without intrinsic performance drawbacks.

cs.PL↗

arXiv2024

A Second Soul: Celebrating the Many Languages of Programming -- Festschrift in Honor of Peter Thiemann's Sixtieth Birthday

This Festschrift is dedicated to Peter Thiemann on the occasion of his sixtieth birthday, celebrating his significant contributions to the field of programming languages. Over the span of more than three decades, Peter has worked on a wide array of topics. This collection of five articles reflects the diversity of his work. The articles cover areas such as partial evaluation and reversible programming, proof assistants and dependent types, discrete mathematics and dynamic programming, functional and object-oriented programming.

cs.PL↗

arXiv2024

Distributed Locking as a Data Type

Mixed-consistency programming models assist programmers in designing applications that provide high availability while still ensuring application-specific safety invariants. However, existing models often make specific system assumptions, such as building on a particular database system or having baked-in coordination strategies. This makes it difficult to apply these strategies in diverse settings, ranging from client/server to ad-hoc peer-to-peer networks. This work proposes a new strategy for building programmable coordination mechanisms based on the algebraic replicated data types (ARDTs) approach. ARDTs allow for simple and composable implementations of various protocols, while making minimal assumptions about the network environment. As a case study, two different locking protocols are presented, both implemented as ARDTs. In addition, we elaborate on our ongoing efforts to integrate the approach into the LoRe mixed-consistency programming language.

cs.PL↗

arXiv2024

Models for Storage in Database Backends

This paper describes ongoing work on developing a formal specification of a database backend. We present the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic models. The first one is a map-based, classical versioned key-value store; the second one, journal-based, appends individual transaction effects to a journal. We formalise a significant part of the specification in the Coq proof assistant. This work will form the basis for a formalisation of a full-fledged backend store with features such as caching or write-ahead logging, as variations on maps and journals.

cs.DB↗

arXiv2023

LoRe: A Programming Model for Verifiably Safe Local-First Software

Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The unpredictability of such interactions paired with their decentralized nature make reasoning about the correctness of local-first software a challenging endeavor. Yet, existing solutions to develop local-first software do not provide support for automated safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions. We propose LoRe, a programming model and compiler that automatically verifies developer-supplied safety properties for local-first applications. LoRe combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We propose a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. Our evaluation shows that LoRe simplifies the development of safe local-first software when compared to state-of-the-art approaches and that verification times are acceptable.

cs.PL↗

arXiv2023

Set-theoretic Types for Erlang

Erlang is a functional programming language with dynamic typing. The language offers great flexibility for destructing values through pattern matching and dynamic type tests. Erlang also comes with a type language supporting parametric polymorphism, equi-recursive types, as well as union and a limited form of intersection types. However, type signatures only serve as documentation, there is no check that a function body conforms to its signature. Set-theoretic types and semantic subtyping fit Erlang's feature set very well. They allow expressing nearly all constructs of its type language and provide means for statically checking type signatures. This article brings set-theoretic types to Erlang and demonstrates how existing Erlang code can be statically typechecked without or with only minor modifications to the code. Further, the article formalizes the main ingredients of the type system in a small core calculus, reports on an implementation of the system, and compares it with other static typecheckers for Erlang.

cs.PL↗

arXiv2019

Antidote SQL: Relaxed When Possible, Strict When Necessary

Geo-replication poses an inherent trade-off between low latency, high availability and strong consistency. While NoSQL databases favor low latency and high availability, relaxing consistency, more recent cloud databases favor strong consistency and ease of programming, while still providing high scalability. In this paper, we present Antidote SQL, a database system that allows application developers to relax SQL consistency when possible. Unlike NoSQL databases, our approach enforces primary key, foreign key and check SQL constraints even under relaxed consistency, which is sufficient for guaranteeing the correctness of many applications. To this end, we defined concurrency semantics for SQL constraints under relaxed consistency and show how to implement such semantics efficiently. For applications that require strict SQL consistency, Antidote SQL provides support for such semantics at the cost of requiring coordination among replicas.

cs.DB↗

arXiv2018

Ensuring referential integrity under causal consistency

Referential integrity (RI) is an important correctness property of a shared, distributed object storage system. It is sometimes thought that enforcing RI requires a strong form of consistency. In this paper, we argue that causal consistency suffices to maintain RI. We support this argument with pseudocode for a reference CRDT data type that maintains RI under causal consistency. QuickCheck has not found any errors in the model.

cs.DC↗

arXiv2018

ACGreGate: A Framework for Practical Access Control for Applications using Weakly Consistent Databases

Scalable and highly available systems often require data stores that offer weaker consistency guarantees than traditional relational databases systems. The correctness of these applications highly depends on the resilience of the application model against data inconsistencies. In particular regarding application security, it is difficult to determine which inconsistencies can be tolerated and which might lead to security breaches. In this paper, we discuss the problem of how to develop an access control layer for applications using weakly consistent data stores without loosing the performance benefits gained by using weaker consistency models. We present ACGreGate, a Java framework for implementing correct access control layers for applications using weakly consistent data stores. Under certain requirements on the data store, ACGreGate ensures that the access control layer operates correctly with respect to dynamically adaptable security policies. We used ACGreGate to implement the access control layer of a student management system. This case study shows that practically useful security policies can be implemented with the framework incurring little overhead. A comparison with a setup using a centralized server shows the benefits of using ACGreGate for scalability of the service to geo-scale.

cs.DB↗

arXiv2018

Just-Right Consistency: reconciling availability and safety

By the CAP Theorem, a distributed data storage system can ensure either Consistency under Partition (CP) or Availability under Partition (AP), but not both. This has led to a split between CP databases, in which updates are synchronous, and AP databases, where they are asynchronous. However, there is no inherent reason to treat all updates identically: simply, the system should be as available as possible, and synchronised just enough for the application to be correct. We offer a principled Just-Right Consistency approach to designing such applications, reconciling correctness with availability and performance, based on the following insights:(i) The Conflict-Free Replicated Data Type (CRDTs) data model supports asynchronous updates in an intuitive and principled way.(ii) Invariants involving joint or mutually-ordered updates are compatible with AP and can be guaranteed by Transactional Causal Consistency, the strongest consistency model that does not compromise availability. Regarding the remaining, "CAP-sensitive" invariants:(iii) For the common pattern of Bounded Counters, we provide encapsulated data type that is proven correct and is efficient; (iv) in the general case, static analysis can identify when synchronisation is not necessary for correctness.Our Antidote cloud database system supports CRDTs, Transactional Causal Consistency and the Bounded Counter data type. Support tools help design applications by static analysis and proof of CAP-sensitive invariants. This system supports industrial-grade applications and has been tested experimentally with hundreds of servers across several geo-distributed data centres.

cs.DC↗

arXiv2017

Techreport: Time-sensitive probabilistic inference for the edge

In recent years the two trends of edge computing and artificial intelligence became both crucial for information processing infrastructures. While the centralized analysis of massive amounts of data seems to be at odds with computation on the outer edge of distributed systems, we explore the properties of eventually consistent systems and statistics to identify sound formalisms for probabilistic inference on the edge. In particular we treat time itself as a random variable that we incorporate into statistical models through probabilistic programming.

cs.DC↗

arXiv2017

Practical Evaluation of the Lasp Programming Model at Large Scale - An Experience Report

Programming models for building large-scale distributed applications assist the developer in reasoning about consistency and distribution. However, many of the programming models for weak consistency, which promise the largest scalability gains, have little in the way of evaluation to demonstrate the promised scalability. We present an experience report on the implementation and large-scale evaluation of one of these models, Lasp, originally presented at PPDP `15, which provides a declarative, functional programming style for distributed applications. We demonstrate the scalability of Lasp's prototype runtime implementation up to 1024 nodes in the Amazon cloud computing environment. It achieves high scalability by uniquely combining hybrid gossip with a programming model based on convergent computation. We report on the engineering challenges of this implementation and its evaluation, specifically related to operating research prototypes in a production cloud environment.

cs.DC↗

arXiv2017

Global-Local View: Scalable Consistency for Concurrent Data Types

Concurrent linearizable access to shared objects can be prohibitively expensive in a high contention workload. Many applications apply ad-hoc techniques to eliminate the need of synchronous atomic updates, which may result in non-linearizable implementations. We propose a new programming model which leverages such patterns for concurrent access to objects in a shared memory system. In this model, each thread maintains different views on the shared object - a thread-local view and a global view. As the thread-local view is not shared, it can be updated without incurring synchronization costs. These local updates become visible to other threads only after the thread-local view is merged with the global view. This enables better performance at the expense of linearizability. We show that it is possible to maintain thread-local views and to perform merge efficiently for several data types and evaluate their performance and scalability compared to linearizable implementations. Further, we discuss the consistency semantics of the data types and the associated programming model.

cs.DC↗