Annette Bieniusa

Elena Yanakieva, Annette Bieniusa, Stefania Dumbrava

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.

Emilie Ma, Ayush Pandey, Annette Bieniusa et al.

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.

Rahul Sharma, Lars Henrich, Larisa Ivanova et al.

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.

Albert Schimpf, Stefan Wehr, Annette Bieniusa

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.