We lay out a new choreographic model that, departing from point-to-point interactions, aims to harness local-first coordination of distributed applications. We dub our model friend-to-friend choreographies since its main application domain are decentralised applications that guarantee confidentiality in a fully decentralisedsetting. A key principle of local-first coordination is indeed that the control on computational resources is not given to third-parties. This yields a notion of projection different than those usually found in the literature since our projection operation aims to identify minimal sets of agents that should be aware of an interaction and so compute the cryptographic keys necessary to ensure confidentiality.Friend-to-friend choreographies have a straightforward implementation in Nearbytes, a platform which provides a communication infrastructure and friend-to-friend decentralised storage.
AI agents are transforming software development from a human-led activity into a collaborative process involving autonomous planners, coders, testers, and reviewers. This shift raises a deceptively simple question with deep engineering and social consequences: when software work is shared between humans and autonomous agents, who is really in charge? This paper argues that the central challenge is coordination: deciding who does what, when, and under whose authority. Natural-language conversation is now the primary medium through which humans and agents interact, assign tasks, and negotiate outcomes; however, conversation is not a substitute for explicit coordination structure.We trace the evolution from Agent-Oriented Software Engineering (AOSE) to contemporary Agentic Software Engineering (ASE), and use a multi-agent code-review scenario to distinguish conversational interaction from governed coordination. The paper argues that autonomy increases the need for coordination; it does not reduce it. Making agentic systems governable therefore requires explicit mechanisms for assigning responsibility, validating outputs, escalating uncertainty, and preserving accountability.We introduce the notion of a runtime coordination contract, a lightweight governance abstraction that specifies roles, task scopes, input/output schemas, escalation conditions, and audit obligations. The paper positions coordination contracts as a runtime analogue of classical coordination and behavioral-contract mechanisms: more flexible than fully pre-designed protocols, but sufficiently explicit to support monitoring and auditability. We discuss some implications for software engineering practice. We conclude proposing an open research agenda concerning contract languages, runtime conformance monitoring, multi-agent benchmarks, and human–agent teaming.
Application placement in distributed cloud-edge environments requires reasoning about where software components are deployed, which resources they consume, and which infrastructure nodes satisfy their deployment policies. This article extends separation logic from program states to application and resource management in cloud-edge settings. Placement states are modelled as component-to-node mappings equipped with node-capacity budgets. Resource separation decomposes both placement mappings and capacity budgets, while separating conjunction enables compositional reasoning about placement assertions. The resulting formal model is complemented by a concise executable specification written in Prolog. We use a motivating scenario to illustrate the logic and its prototype, and then revisit the same scenario as a continuous-reasoning use case. Finally, we evaluate the scalability of our prototype through simulation-based experiments comparing local repair enabled by continuous reasoning with complete re-placement over lifelike cloud-edge infrastructures.
A full-abstraction theorem for a natural translation from the polyadic π-calculus to a subcalculus of the asynchronous monadic π-calculus is proved: two terms of the polyadic calculus are barbed congruent iff their translations are barbed congruent in the subcalculus. The subcalculus is defined by means of a type system for asynchronous monadic processes. The class of well-typed asynchronous monadic contexts strictly includes the translations of polyadic contexts.
The verification of large codebases requires compositional analysis techniques that enable the reuse and composition of summaries previously computed for unchanged procedures or code fragments. This observation is essential for scalable program analysis and lies at the core of Separation Logic approaches. Local reasoning in Separation Logic relies on computing code summaries with minimal hypotheses about the memory locations accessed by a program fragment and then exploiting frame inference to compose specifications over larger heaps. Bi-abduction algorithms are instrumental for the automation of frame inference, as they synthesize both the missing resources required to meet a specification and the portion of memory that remains unaffected by execution. Bi-abduction was originally introduced for forward over-approximate reasoning. More recently, it has been adapted to forward under-approximate incorrectness analyses for automatic bug detection. In this paper we formalize bi-abduction within a fully general setting that is independent of both the analysis direction (forward or backward) and the sense of approximation (over or under). We first instantiate this framework to derive bi-abduction algorithms for backward analyses, encompassing both under- and over-approximate reasoning. We then propose a novel notion of full bi-abduction that is independent of both the analysis direction and the approximation discipline, yielding a single sound framework for compositional reasoning across all four combinations of forward/backward and over-/under-approximate analyses. We provide a proof-of-concept implementation of the proposed algorithms and use it to reproduce the examples presented in the paper.
