Search Results

Documents authored by Kuhn, Roland

Document
DOI: 10.4230/LIPIcs.ECOOP.2026.7
Compositional Design, Implementation, and Verification of Swarms

Authors: Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.
Cite as

Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional Design, Implementation, and Verification of Swarms. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 7:1-7:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{furbach_et_al:LIPIcs.ECOOP.2026.7,
  author =	{Furbach, Florian and Clorius, Lucas and Kuhn, Roland and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  title =	{{Compositional Design, Implementation, and Verification of Swarms}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{7:1--7:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.7},
  URN =		{urn:nbn:de:0030-drops-261036},
  doi =		{10.4230/LIPIcs.ECOOP.2026.7},
  annote =	{Keywords: Swarms, Swarm Protocols, Concurrency, Distributed Coordination, Local-first Software, Behavioural Types, Publish-Subscribe, Asynchronous Communication}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.18
Compositional Design, Implementation, and Verification of Swarms (Artifact)

Authors: Lucas Clorius, Florian Furbach, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This is the companion artifact of the paper titled "Compositional Design, Implementation, and Verification of Swarms" (ECOOP'26). This artifact contains an extension of the open-source Actyx toolkit that implements the theoretical results in the paper. It also includes scripts to reproduce all experiments and claims in Section 6 of the paper, as well as documentation on the usage of our extended Actyx toolkit via various examples.
Cite as

Lucas Clorius, Florian Furbach, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional Design, Implementation, and Verification of Swarms (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 18:1-18:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{clorius_et_al:DARTS.12.1.18,
  author =	{Clorius, Lucas and Furbach, Florian and Kuhn, Roland and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  title =	{{Compositional Design, Implementation, and Verification of Swarms (Artifact)}},
  pages =	{18:1--18:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Clorius, Lucas and Furbach, Florian and Kuhn, Roland and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.18},
  URN =		{urn:nbn:de:0030-drops-261559},
  doi =		{10.4230/DARTS.12.1.18},
  annote =	{Keywords: Swarms, Swarm Protocols, Concurrency, Distributed Coordination, Local-first Software, Behavioural Types, Publish-Subscribe, Asynchronous Communication}
}
Document
DOI: 10.4230/DagRep.14.1.108
Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051)

Authors: Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann

Published in: Dagstuhl Reports, Volume 14, Issue 1 (2024)

Abstract
The emergence of new computing systems, like cloud computing, blockchains, and Internet of Things (IoT), replaces the traditional monolithic software hardware stack with a distributed heterogeneous model. This change poses new demands on the programming languages for developing such systems: compositionality, allowing decomposition of a system into smaller, possibly heterogeneous, parts and composition of the individually verified parts into a verified whole, security, asserting end-to-end integrity and confidentiality, quantitative reasoning methods, accounting for timing and probabilistic events, and, as a cross-cutting concern, certification of asserted properties in terms of independently verifiable, machine-checked proofs. Characteristics of this emerging computation model are distribution of the participating entities and message passing as the primary means of communication. Message passing is also the communication model underlying behavioral types and programming languages, making them uniquely fitted for this new application domain. Behavioral types explicitly capture the protocols of message exchange and have a strong theoretical foundation. Recent applications of behavioral types include smart contract languages, information flow control, and machine-checked proofs of safety properties. Although these early explorations are promising, the current state of the art of behavioral types and programming languages lacks a comprehensive account of the above-mentioned demands. This Dagstuhl Seminar aims to gather experts from academia and industry to discuss the use of programming languages tailored to tackle the challenges posed by today’s emerging distributed and heterogeneous computing platforms, e.g., by making use of behavioral types. It will focus on static and possibly dynamic mechanisms to support compositionality, security, quantitative reasoning, and certification.
Cite as

Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann. Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051). In Dagstuhl Reports, Volume 14, Issue 1, pp. 108-129, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{balzer_et_al:DagRep.14.1.108,
  author =	{Balzer, Stephanie and Carbone, Marco and Kuhn, Roland and Thiemann, Peter},
  title =	{{Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051)}},
  pages =	{108--129},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{1},
  editor =	{Balzer, Stephanie and Carbone, Marco and Kuhn, Roland and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.108},
  URN =		{urn:nbn:de:0030-drops-204930},
  doi =		{10.4230/DagRep.14.1.108},
  annote =	{Keywords: behavioural types, concurrency, programming languages, session types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.15
Behavioural Types for Local-First Software

Authors: Roland Kuhn, Hernán Melgratti, and Emilio Tuosto

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification. Our model elaborates on the Actyx industrial platform and provides the basis for tool support: we sketch an implemented prototype which proves this work a viable step towards reasoning about local-first and peer-to-peer software systems.
Cite as

Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kuhn_et_al:LIPIcs.ECOOP.2023.15,
  author =	{Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
  title =	{{Behavioural Types for Local-First Software}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.15},
  URN =		{urn:nbn:de:0030-drops-182086},
  doi =		{10.4230/LIPIcs.ECOOP.2023.15},
  annote =	{Keywords: Distributed coordination, local-first software, behavioural types, publish-subscribe, asynchronous communication}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.14
Behavioural Types for Local-First Software (Artifact)

Authors: Roland Kuhn, Hernán Melgratti, and Emilio Tuosto

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
This artifact supports the theory of swarm protocols presented in the related article. Specifically, following the top-down development typical of choreographic approaches, our artifact enables the specification of systems of peers communicating through an event notification mechanism from a global viewpoint which can then be projected to local specifications of peers, rendered as machines. To the best of our knowledge, ours is the first implementation of a behavioural type framework supporting the application of the principles of local-first software for network devices which collaborate on a common task while retaining full autonomy. The artifact can be integrated in the Actyx industrial platform; this proves this work a viable step towards reasoning about local-first and peer-to-peer software systems.
Cite as

Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{kuhn_et_al:DARTS.9.2.14,
  author =	{Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
  title =	{{Behavioural Types for Local-First Software (Artifact)}},
  pages =	{14:1--14:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Kuhn, Roland and Melgratti, Hern\'{a}n and Tuosto, Emilio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.14},
  URN =		{urn:nbn:de:0030-drops-182541},
  doi =		{10.4230/DARTS.9.2.14},
  annote =	{Keywords: Distributed coordination, local-first software, behavioural types, publish-subscribe, asynchronous communication}
}
Document
DOI: 10.4230/DagRep.11.8.52
Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372)

Authors: Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas

Published in: Dagstuhl Reports, Volume 11, Issue 8 (2022)

Abstract
Behavioural types specify the way in which software components interact with one another. Unlike data types (which describe the structure of data), behavioural types describe communication protocols, and their verification ensures that programs do not violate such protocols. The behavioural types research community has developed a flourishing literature on communication-centric programming, exploring many directions. One of the most studied behavioural type systems are session types, introduced by Honda et al. in the ‘90s, and awarded with prizes for their influence in the past 20 and 10 years (by the ESOP and POPL conferences, respectively). Other varieties of behavioural types include typestate systems, choreographies, and behavioural contracts; research on verification techniques covers the spectrum from fully static verification at compile-time to fully dynamic verification at run-time. In the last decade, research on behavioural types has shifted emphasis towards practical applications, using both novel and existing programming languages (e.g., Java, Python, Go, C, Haskell, OCaml, Erlang, Scala, Rust). An earlier Dagstuhl Seminar, 17051 "Theory and Applications of Behavioural Types" (January 29-February 3, 2017), played an important role in coordinating this effort. Yet, despite the vibrant community and the stream of new results, the use of behavioural types for mainstream software development and verification remains limited. This limitation is largely down to the rapid pace at which mainstream industrial practice for the design and development of concurrent and distributed systems evolves, often resulting in substantial divergence from academic research. In the absence of established tools to express communication protocols, widely used implementations concentrate solely on scalability and reliability. The flip side is that these systems are either overly loose, supporting any conceivable communication structure (via brokers), or overly restricted, supporting only simple request-response protocols (like HTTP or RPC). In this seminar, experts from academia and industry explored together how best to bridge the gap between theory and mainstream practice. They tackled challenges that are fundamental in practical systems development, but are rarely or only partially addressed in the behavioural types literature - in particular, failure handling, asynchronous communication, and dynamic reconfiguration. Moreover they explored how the tools of behavioural types and programming languages theory (such as linearity, gradual types, and dependent types) can help to address these challenges.
Cite as

Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas. Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372). In Dagstuhl Reports, Volume 11, Issue 8, pp. 52-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{dezani_et_al:DagRep.11.8.52,
  author =	{Dezani, Mariangiola and Kuhn, Roland and Lindley, Sam and Scalas, Alceste},
  title =	{{Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372)}},
  pages =	{52--75},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{8},
  editor =	{Dezani, Mariangiola and Kuhn, Roland and Lindley, Sam and Scalas, Alceste},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.8.52},
  URN =		{urn:nbn:de:0030-drops-157699},
  doi =		{10.4230/DagRep.11.8.52},
  annote =	{Keywords: behavioural types, concurrency, programming languages, session types}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact