activity
20232026
collaborators
Showing cs.PLShow all

7 papers · 1 filter

cs.PL2026

GUARDTs: Decentralized Access Control for Replicated Data Types

Christian Kuessner, Ragnar Mogk, Julian Haas +2

Replicated data types providing strong eventual consistency offer a principled foundation for developing decentralized software. Yet existing approaches to programming such data ty…

cs.PL2026

On Eliminating the Impossible with Dependent Types: Choreographic Libraries with Proof-Carrying Located Values

Simon Daniel, Timon Böhler, David Richter +2

With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. When implementing a distributed protocol, developers must ensure…

cs.PL2026

Mechanizing Choreographic Programs and Hoare Logic with State Transformers

Timon Böhler, Simon Daniel, David Richter +2

Choreographic programming is a programming model for developing distributed applications where an entire communication protocol is written as a single program, which a compiler the…

cs.PL2025

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

Julian Haas, Ragnar Mogk, Annette Bieniusa +1

Consensus protocols are fundamental in distributed systems as they enable services with strong consistency properties. However, designing protocols optimized for specific use-cases…

cs.PL2024

Compiling with Arrays

David Richter, Timon Böhler, Pascal Weisenburger +1

Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and r…

cs.PL2024

Distributed Locking as a Data Type

Julian Haas, Ragnar Mogk, Annette Bieniusa +1

Mixed-consistency programming models assist programmers in designing applications that provide high availability while still ensuring application-specific safety invariants. Howeve…

cs.PL2023

A Direct-Style Effect Notation for Sequential and Parallel Programs

David Richter, Timon Böhler, Pascal Weisenburger +1

Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provi…