arXiv subjects

Jonas Kastberg Hinrichsen

Publications and source records attributed to Jonas Kastberg Hinrichsen.

3 recordsLinked to original sources

arXiv2026

Beyond Platforms -- Growing Distributed Transaction Networks for Digital Commerce

We talk of the internet as digital infrastructure; but we leave the building of rails and roads to the quasi-monopolistic platform providers. Decentralised architectures provide a number of advantages: They are potentially more inclusive for small players; more resilient against adversarial events; and seem to generate more innovation. However, it is not well understood how to evolve, adapt and govern decentralised infrastructures. This article reports qualitative empirical research on the development and governance of the Beckn Protocol, an open source protocol for decentralised transactions, the successful development of domain-specific adaptations, and implementation and scaling of commercial infrastructures based on it. It explores how the architecture and governance support local innovation for specific business domains, and how the domain-specific innovations feed back into the development of the core concept The research applied a case study approach, combining interviews with core members of the Beckn community; triangulated by interviews with community leaders of domain specific adaptations and by analysis of online documents and the protocol itself. The article shows the possibility of such a decentralised approach to IT Infrastructures. It analyses the Beckn Protocol, domain specific adaptations, and networks built as a software ecosystem. Based on this analysis, a number of generative mechanisms, socio-technical arrangements that support adoption, innovation, and scaling of infrastructures are highlighted.

cs.CY↗

arXiv2024

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step-indexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly simple class of safety properties. In this paper, we explore if and how intensional refinement is a viable methodology for strengthening higher-order concurrent (and distributed) separation logic to prove non-trivial safety and liveness properties. Specifically, we introduce Trillium, a language-agnostic separation logic framework for showing intensional refinement relations between traces of a program and a model. We instantiate Trillium with a concurrent language and develop Fairis, a concurrent separation logic, that we use to show liveness properties of concurrent programs under fair scheduling assumptions through a fair liveness-preserving refinement of a model. We also instantiate Trillium with a distributed language and obtain an extension of Aneris, a distributed separation logic, which we use to show refinement relations between distributed systems and TLA+ models.

cs.PL↗

arXiv2022

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic

Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism -- based on session types -- for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a channel-based merge sort, a channel-based load-balancing mapper, and a variant of the map-reduce model, using concise specifications. While Actris was already presented in a conference paper (POPL'20), this paper expands the prior presentation significantly. Moreover, it extends Actris to Actris 2.0 with a notion of subprotocols -- based on session-type subtyping -- that permits additional flexibility when composing channel endpoints, and that takes full advantage of the asynchronous semantics of message passing in Actris. Soundness of Actris 2.0 is proven using a model of its protocol mechanism in the Iris framework. We have mechanised the theory of Actris, together with custom tactics, as well as all examples in the paper, in the Coq proof assistant.

cs.LO↗