# Volition Elicitation: Operational Semantics for People and Their Machines

arXiv: https://arxiv.org/abs/2607.14138 · HTML: https://mlsanity.com/paper/2607.14138/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 54 references that are in the map.
- First posted on arXiv 10 Jul 2026.

## Builds on (most cited first, 9 of 9)

- [Hazelnut: A Bidirectionally Typed Structure Editor Calculus](https://mlsanity.com/paper/1607.04180/) (2016)
- [Interaction Trees: Representing Recursive and Impure Programs in Coq](https://mlsanity.com/paper/1906.00046/) (2019)
- [Foundations for Grassroots Democratic Metaverse](https://mlsanity.com/paper/2203.04090/) (2022)
- [Grassroots Social Networking: Where People have Agency over their Personal Information and Social Graph](https://mlsanity.com/paper/2306.13941/) (2023)
- [Grassroots Flash: A Payment System for Grassroots Cryptocurrencies](https://mlsanity.com/paper/2309.13191/) (2023)
- [Grassroots Platforms with Atomic Transactions: Social Networks, Cryptocurrencies, and Democratic Federations](https://mlsanity.com/paper/2502.11299/) (2025)
- [A Grassroots Architecture to Supplant Global Digital Platforms by a Global Digital Democracy](https://mlsanity.com/paper/2404.13468/) (2024)
- [Characterising Global Platforms: Centralised, Decentralised, Federated, and Grassroots](https://mlsanity.com/paper/2511.03286/) (2025)
- [Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI (Full Version)](https://mlsanity.com/paper/2602.06934/) (2026)

## Abstract (arXiv)

The most prevalent distributed systems today include people and their personal machines (smartphones), and computations in them are driven by people's volitions. Volition-guarded multiagent atomic transactions were proposed as an abstract specification language for such systems, in which a transaction has a precondition on the machine states of its participants and is guarded by the volitions of some of them. Here we develop an abstraction cascade that derives smartphone apps from such specifications and prove it correct down to the base programming language, GLP. The cascade consists of: (1) communicating volitional agents (CVA), which implement every local volition-guarded specification with simple guards, correctly, and completely for its strongly fair runs, by two-phase commit coordinated by the initiating agent; (2) volition-guarded GLP (vGLP), an extension of GLP with volitional procedures, whose goals put an interactively-typed question to the person, into which that implementation compiles; and (3) GLP, which implements vGLP by eliciting the person's answers through the widgets of their interactive types, correctly, and completely for complete widgets. We demonstrate the approach on three grassroots platforms --- a social graph, a social network, and currencies: a compiler carries the social graph and the currencies down the cascade to GLP programs that run with scripted persons, and earlier programs of the three run as mini-apps of one smartphone app.