MSc Mirko Köhler

Hochschulstr. 10
64289 Darmstadt, Germany

I work on programming abstractions for replicated data. Currently, I’m the main contributor to ConSysT, an object-oriented language for mixed consistency with replicated objects. My research interests include concurrency, mixed consistency protocols, and type systems.

Publications

CAPE - European Open Compute Architecture for Powerful Edge

Martin Kaiser, Lennart Tigges, Jens Hagemeyer, Christian Klarhorst, Björn Voß, Fred Buining, Bola Fakhoury, János Lazányi, René Griessl, Muhammad Shahzad, Yiannis Georgiou, Salim Mimouni, Pedro Velho, Michael Mercier, Eva Trungel, Julian Gajewski, Stefan Krupop, Michavor Dem Berge, Deepak M. Mathew, Skipis Dimitrios, Arnidis Iordanis, Orestis Vantzos, David Georgantas, Gautier Rouaze, Christoph Bühler, Guido Salvaneschi, Brandon Lewis, Angela Hauber

In 2025 28th Euromicro Conference on Digital System Design (DSD), 2025

Abstract PDF

CAPE is a European-funded project targeting to reshape edge-cloud computing by defining edge micro data centers as a new unit of computing. Fully committing to open source, CAPE develops a fully Composable Infrastructure (CI) for high-performance edge server hardware platforms grounded in open, forward-looking standards. Together with an open-source software stack covering the Edge-Cloud Continuum, this holistic approach boosts power and energy efficiency while reducing resource overprovisioning. Completely based on open standards, CAPE strengthens the digital sovereignty Europe needs in a challenging future. This work gives an overview of the current architectural blueprint of the project, focusing on integrating game-changing technologies like Compute Express Link (CXL) for compute and memory disaggregation, pushing open source cluster management, and AI-assisted deployment software stacks using Infrastructure from Code (IfC). The proposed approaches and benefits for future Edge-Cloud data centers are demonstrated within three use cases, ranging from Smart Grid and Edge-AI to Satellite Data Processing.
MSR

TerraDS: A Dataset for Terraform HCL Programs

Christoph Bühler, David Spielmann, Roland Meier, Guido Salvaneschi

In Proceedings of the IEEE/ACM 22nd International Conference on Mining Software Repositories, MSR, 2025

Abstract PDF

Infrastructure as Code (IaC) aims to automate infrastructure management by enabling the definition of infrastructure configurations in programs, rather than manually configuring hardware or cloud resources. Terraform is one of the most widely used IaC tools, gaining significant traction in recent years, as highlighted by its large and active user community and widespread adoption in both open-source and enterprise environments. Terraform’s code is written in the HashiCorp Configuration Language (HCL), which defines the infrastructure in a declarative manner. Despite the widespread adoption of Terraform, there is no large-scale dataset available for researchers to study IaC Terraform programs systematically. To address this gap, we present TerraDS, the first dataset of publicly available Terraform programs written in HCL. TerraDS contains the HCL code and the metadata of 67,360 open source repositories with permissive open-source licenses. The dataset includes 279,344 Terraform modules with 1,773,991 registered resources, all compiled into a reusable archive ( 335 MB).
TSE
ConSysT

Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications

Mirko Köhler, George Zakhour, Pascal Weisenburger, Guido Salvaneschi

IEEE Transactions on Software Engineering 51 (1), 2024

Abstract PDF

Local-first software embraces data replication as a means to achieve scalability and offline availability. A crucial ingredient of local-first software are mergeable data types, like conflict-free replicated data types (CRDTs), which feature eventual consistency by enabling processes to access data locally and later merge it with other replicas in an asynchronous manner. Notably, the merging process needs to adhere to application constraints for correctness. Ensuring such application-level invariants poses a challenge, as developers must reason about the replicated program state and resort to manual synchronization of specific application components to enforce the invariant.
This paper introduces ConLoc (Consistent Local-First Software), a novel system designed to automatically enforce safety and maintain invariants in local-first applications. ConLoc effectively addresses the issue of preserving invariants in the execution of programs with replicated data types, including CRDTs. Our approach is able to verify the correctness of many CRDTs examined in the literature and in implementations, such the ones used in the Riak database. ConLoc ensures that applications are automatically synchronized correctly, resulting in substantial latency and throughput improvements when compared to sequential execution, while upholding the same set of invariants.
ECOOP

Compiling with Arrays

David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2024

Abstract PDF Supp

Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables.
The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (AiNF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. AiNF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to AiNF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
SPLASH Companion
ConSysT

Safe Combination of Data-Centric and Operation-Centric Consistency

Mirko Köhler, Guido Salvaneschi

In Companion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH Companion, 2023

Abstract PDF

Programming distributed systems requires maintaining consistency among data replicas. In recent years, various frameworks have proposed language-level abstractions for this, falling into two fundamental approaches: data-centric and operation-centric solutions. The former allow developers to explicitly assign consistency levels to data, the latter enable attaching consistency constraints to operations. In practice, developers may benefit from both in the same application: data-centric consistency harmonizes well with object-oriented programming, yet one may need the flexibility to access the same data with a different consistency level depending on the operation. Currently, there is no solution that integrates both: it is a conceptual challenge to unify these two models and design a type system capable of ensuring their correct interaction.
We present ConOpY, a programming language that integrates both data-centric and operation-centric consistency into the same design. The ConOpY type system guarantees the proper usage of consistency levels, preventing consistency violations resulting from an improper mix of consistency models. ConOpY is implemented as a Java extension based on annotations.
ECOOP

A Direct-Style Effect Notation for Sequential and Parallel Programs

David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

In Proceedings of the 37th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2023

Abstract PDF Supp

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 provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code.
In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.
OOPSLA
ConSysT

Rethinking Safe Consistency in Distributed Object-Oriented Programming

Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 4 (OOPSLA), 2020

Abstract PDF

Large scale distributed systems require to embrace the trade off between consistency and availability, accepting lower levels of consistency to guarantee higher availability. Existing programming languages are, however, agnostic to this compromise, resulting in consistency guarantees that are the same for the whole application and are implicitly adopted from the middleware or hardcoded in configuration files.
In this paper, we propose to integrate availability in the design of an object-oriented language, allowing developers to specify different consistency and isolation constraints in the same application at the granularity of single objects. We investigate how availability levels interact with object structure and define a type system that preserves correct program behavior. Our evaluation shows that our solution performs efficiently and improves the design of distributed applications.
FTfJP
ConSysT

ConSysT: Tunable, Safe Consistency Meets Object-Oriented Programming

Mirko Köhler, Nafise Eskandani, Alessandro Margara, Guido Salvaneschi

In Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP, 2020

Abstract

Data replication is essential in scenarios like geo-distributed datacenters, but poses challenges for data consistency. Developers adopt Strong consistency at the cost of performance or embrace Weak consistency and face a higher programming complexity. We argue that languages should associate consistency to data types. We present , a programming language and middleware that provides abstractions to specify consistency types, enabling mixing different consistency levels in the same application. Such mechanism is fully integrated with object-oriented programming and type system guarantees that different levels can only be mixed correctly.
ASE

Automated Refactoring to Reactive Programming

Mirko Köhler, Guido Salvaneschi

In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, ASE, 2019

Abstract PDF

Reactive programming languages and libraries, such as ReactiveX, have been shown to significantly improve software design and have seen important industrial adoption over the last years. Asynchronous applications - which are notoriously error-prone to implement and to maintain - greatly benefit from reactive programming because they can be defined in a declarative style, which improves code clarity and extensibility.
In this paper, we tackle the problem of refactoring existing software that has been designed with traditional abstractions for asynchronous programming. We propose 2Rx, a refactoring approach to automatically convert asynchronous code to reactive programming. Our evaluation on top-starred GitHub projects shows that 2Rx is effective with common asynchronous constructs and it can provide a refactoring for 91.7% of their occurrences.
SPLASH Companion
ConSysT

Distributed Object-Oriented Programming with Multiple Consistency Levels in ConSysT

Nafise Eskandani, Mirko Köhler, Alessandro Margara, Guido Salvaneschi

In Companion Proceedings of the 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH Companion, 2019

Abstract

Data replication is essential in scenarios like geo-distributed datacenters and edge computing. Yet, it poses a challenge for data consistency. Developers either adopt high consistency at the detriment of performance or they embrace low consistency and face a much higher programming complexity. We argue that language abstractions should support associating the level of consistency to data types. We present ConSysT, a programming language and middleware that provides abstractions to specify consistency types, enabling mixing different consistency levels in the same application. Such mechanism is fully integrated with object-oriented programming and type system guarantees that different levels can be mixed only in a correct way.
OOPSLA

Language-Integrated Privacy-Aware Distributed Queries

Guido Salvaneschi, Mirko Köhler, Daniel Sokolowski, Philipp Haller, Sebastian Erdweg, Mira Mezini

Proceedings of the ACM on Programming Languages 3 (OOPSLA), 2019

Abstract PDF

Distributed query processing is an effective means for processing large amounts of data. To abstract from the technicalities of distributed systems, algorithms for operator placement automatically distribute sequential data queries over the available processing units. However, current algorithms for operator placement focus on performance and ignore privacy concerns that arise when handling sensitive data.
We present a new methodology for privacy-aware operator placement that both prevents leakage of sensitive information and improves performance. Crucially, our approach is based on an information-flow type system for data queries to reason about the sensitivity of query subcomputations. Our solution unfolds in two phases. First, placement space reduction generates deployment candidates based on privacy constraints using a syntax-directed transformation driven by the information-flow type system. Second, constraint solving selects the best placement among the candidates based on a cost model that maximizes performance. We verify that our algorithm preserves the sequential behavior of queries and prevents leakage of sensitive data. We implemented the type system and placement algorithm for a new query language SecQL and demonstrate significant performance improvements in benchmarks.
OOPSLA
ScalaLoci

Distributed System Development with ScalaLoci

Pascal Weisenburger, Mirko Köhler, Guido Salvaneschi

Proceedings of the ACM on Programming Languages 2 (OOPSLA), 2018

Abstract PDF Code Website

Distributed applications are traditionally developed as separate modules, often in different languages, which react to events, like user input, and in turn produce new events for the other modules. Separation into components requires time-consuming integration. Manual implementation of communication forces programmers to deal with low-level details. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole. The ScalaLoci distributed programming language addresses these issues with a coherent model based on placement types that enables reasoning about distributed data flows, supporting multiple software architectures via dedicated language features and abstracting over low-level communication details and data conversions. As we show, ScalaLoci simplifies developing distributed systems, reduces error-prone communication code and favors early detection of bugs.
OOPSLA

i3QL: Language-Integrated Live Data Views

Ralf Mitschke, Sebastian Erdweg, Mirko Köhler, Mira Mezini, Guido Salvaneschi

In Proceedings of the 2014 ACM International Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA, 2014

Abstract PDF

An incremental computation updates its result based on a change to its input, which is often an order of magnitude faster than a recomputation from scratch. In particular, incrementalization can make expensive computations feasible for settings that require short feedback cycles, such as interactive systems, IDEs, or (soft) real-time systems.
This paper presents i3QL, a general-purpose programming language for specifying incremental computations. i3QL provides a declarative SQL-like syntax and is based on incremental versions of operators from relational algebra, enriched with support for general recursion. We integrated i3QL into Scala as a library, which enables programmers to use regular Scala code for non-incremental subcomputations of an i3QL query and to easily integrate incremental computations into larger software projects. To improve performance, i3QL optimizes user-defined queries by applying algebraic laws and partial evaluation. We describe the design and implementation of i3QL and its optimizations, demonstrate its applicability, and evaluate its performance.