Pact: A Choreographic Language for Agentic Ecosystems
arXiv:2605.03143v1 [cs.PL] 4 May 2026
KIRAN GOPINATHAN, Basis Research Institute, USA JACK FESER, Basis Research Institute, USA MICHELANGELO NAIM, Basis Research Institute, USA ZENNA TAVARES, Basis Research Institute, USA ELI BINGHAM, Basis Research Institute, USA Recent advances in large language models have led to the rise of software systems (i.e. agents) that execute with increasing autonomy on behalf of users in open, multi-party settings, interacting with untrusted counterparts and managing private information. Choreographic programming offers correct-by-construction protocoldesign for such settings, but assumes cooperative participants — it has no notion of agent self-interest, that is, why an agent will follow a protocol. In this talk we introduce Pact, a choreographic language extended with operations to describe agent choices and preferences, drawing from the rich literature of game theory. Every Pact protocol maps to a formal game, allowing protocol designers to reason about game-theoretic properties of their protocols, such as solving for decision policies. We present Pact’s design and a preliminary implementation — a bounded-rational solver that computes decision policies over Pact protocols — and findings from applying this language to multi-party coordination with self-interested agentic participants. Additional Key Words and Phrases: Choreographic programs, Protocols, LLMs, Multi-agentic Protocols ACM Reference Format: Kiran Gopinathan, Jack Feser, Michelangelo Naim, Zenna Tavares, and Eli Bingham. 2026. Pact: A Choreographic Language for Agentic Ecosystems. In Proceedings of 2nd International Workshop on Choreographic Programming (CP’26). ACM, New York, NY, USA, 8 pages. https://doi.org/10.1145/nnnnnnn.nnnnnnn
1
Introduction
Advances in large language models have led to the rise of autonomous agents that execute increasingly autonomously on behalf of users in open, multi-party settings, interacting with untrusted counterparts and managing private information. While LLM-based AI is capable, in practice it is rarely trustworthy, especially when it must negotiate with unpredictable, possibly hostile, other agents. Evidence of this is already abundant: agents are systematically vulnerable to prompt injection attacks [11, 16], they regularly exhibit sycophantic behaviour that undermines rational reasoning, and they can easily be coerced into acting against their own best interests [1, 2]. If these ecosystems are to be sustainable, agents urgently need tools to manage these interactions. Trust in multi-party systems fundamentally boils down to coordination, and problems of coordination are well studied in the PL literature. Choreographic programming [18] describes one such formalism for this purpose, designed in such a way that choreographic programs are correct by Authors’ Contact Information: Kiran Gopinathan, [email protected], Basis Research Institute, New York, New York, USA; Jack Feser, [email protected], Basis Research Institute, New York, New York, USA; Michelangelo Naim, [email protected], Basis Research Institute, New York, New York, USA; Zenna Tavares, [email protected], Basis Research Institute, New York, New York, USA; Eli Bingham, [email protected], Basis Research Institute, New York, New York, USA. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. CP’26, Boulder, CO © 2026 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-x-xxxx-xxxx-x/YYYY/MM https://doi.org/10.1145/nnnnnnn.nnnnnnn , Vol. 1, No. 1, Article . Publication date: May 2026.
2
Gopinathan et al.
Choreography (* title : string @ buyer, budget : int @ buyer book : Book @ seller *) let bookseller () = send(title, seller) price = seller.price_of(title) send(price, buyer) if broadcast(price < budget) then exchange( buyer, seller, book, price )
Buyer
Seller
(* title : string, budget : int *)
(* book : Book *)
let bookseller_buyer () = send(title, seller) price = recv(seller) choice = price < budget send(choice, seller) if choice then begin book = recv(seller) book = send(price, seller) end
let bookseller_seller () = title = recv(buyer) price = price_of(title) send(price, buyer) choice = recv(buyer) if choice then begin send(book, buyer) balance += recv(buyer) end
Fig. 1. A choreographic bookseller protocol (left) and its endpoint projections for buyer (middle) and seller (right). The choreography compiles to local programs, guaranteeing deadlock-freedom by construction.
construction—guaranteed to be deadlock-free. Implementations and embeddings of choreographic programs now exist in several production languages [5, 13, 20] and the area is rapidly maturing. Recent work has begun investigating enriching them with various cryptographic primitives [19, 22], extending them towards adversarial settings where participants may not be trusted to execute faithfully, opening the door to the use of choreographies to manage multi-agentic coordination. Could choreographies be used to reason about agentic interactions? Consider Figure 1 (left), which describes a canonical choreography “hello world”—a book seller protocol. The choreography describes an interaction between two parties—a buyer and a seller: the buyer sends a title to the seller, and the seller, computing a price locally, responds back to the buyer. If the price is within budget, both parties conduct an exchange and the book is sold. The choreographic language guarantees deadlock freedom, and this choreography can be compiled via endpoint projection to local programs where every send is matched by a corresponding receive by the other parties. While this choreography captures the communication pattern between the two parties precisely, this program fails to capture a crucial aspect of agentic interactions: why would any agent follow this protocol? Agents operating in such ecosystems have conflicting objectives, i.e. a buyer wants the cheapest price for a good, the seller wants the most profit, and will only participate in protocols that serve their objectives. Choreographies specify the structure of interaction, but have no model of preferences, and so provide no help in reasoning about such questions. In this paper, we present Pact, a choreographic language that adds three constructs to facilitate agentic coordination: explicit agent choices, where agents make strategic decisions within a protocol (i.e., what price to sell a book at, what price to purchase); explicit agent utilities, where agents declare what they value about outcomes (i.e., how much an agent values the quality of the book they receive), and nature variables, which model agent priors about the world (i.e. assumptions about the distribution of book quality). Every Pact protocol maps unambiguously to a formal game, and agent preferences and decisions are made explicit and targets of formal reasoning. Agents can use Pact protocols as a medium for negotiation, proposing and analysing these programs collaboratively to facilitate large scale ecosystems of autonomous agents. In summary, the key contributions of this work are: • Identification of game-theoretic reasoning as a natural extension of choreographic programming, enabling its application to the rapidly emerging domain of multi-agentic coordination. • The initial design of Pact, a choreographic language with semantics grounded in game theory. • An example game-theoretic decision policy solver built as an analysis on top of Pact programs. The rest of this paper is organised as follows: Section 2 walks through the design of Pact by example, extending the bookseller choreography with choices, utilities and nature variables; , Vol. 1, No. 1, Article . Publication date: May 2026.
Pact: A Choreographic Language for Agentic Ecosystems
3
Section 3 presents a game-theoretic analysis built on top of Pact, using theory-of-mind models to construct a bounded-rational decision policy solver for Pact programs; Section 4 presents a brief survey of the relevant literature around formalising games and agentic coordination, and Section 5 concludes this work and outlines directions of future work we are investigating. 2
How to Forge a Pact
We now walk through the design of Pact by extending the bookseller choreography (cf. Figure 1) incrementally to address concerns relevant in multi-agentic coordination. Each extension extends the language to capture an additional aspect of agentic interaction: (1) explicit modeling of agent choices, (2) encoding of agent utilities, and (3) representation of priors using nature variables. By the end of this section, the bookseller protocol in Pact will correspond to a complete formal game. 2.1
Making Strategic Choices Explicit
To make our choreographies useful for agentic interactions, let bookseller () = send(title, seller) we must be able to analyse them as games, and the core of any price = seller.choose(float) game is about the strategic choices of its participants — how send(price, buyer) if broadcast(buyer.choose(bool)) each participant will make choices taking into consideration the then exchange( actions of others. Our initial book seller choreography in some buyer, seller, book, price sense is too prescriptive: it states exactly how each agent will ) compute its local choices, that the seller will use the price given by its function price_of, and the buyer will purchase the good if the price is less than its budget. But is this accurate in an agentic setting? Can we trust the seller to not adjust the price based on their beliefs about the buyer? Similarly, will the buyer purchase the book for any price within budget? To capture the strategic nature of this interaction, the first thing we must do is make the choices of each participant explicit: we replace each agent’s hardcoded choices with a agent.choose method. In terms of the dynamic semantics of the language, we model these as non-deterministic choices, underspecified by the language, but relevant for game-theoretic analyses. 2.2
Encoding Agent Utilities
Our choice operator tells us what agents decide, but not why. let bookseller () = buyer.values(book.quality) In our original protocol, the value gained by the seller through send(title, seller) participating in the protocol was clear, the price it received from price = seller.choose(float) send(price, buyer) the buyer as the fourth argument to exchange, but what does if broadcast(buyer.choose(bool)) the buyer gain? To reason about such strategic decisions, our then exchange( buyer, seller, language needs some model of agent objectives. We draw from book, price game theory and equip each agent with utility functions over ) outcomes, encoding our beliefs of what each participant stands to gain or lose from a protocol’s execution. We assume an abstract notion of money which is valued by all participants, capturing the monetary gain of the seller. The values operator declares an agent’s utility: writing buyer.values(book.quality) states that the buyer’s payoff from this interaction also depends on the quality of the book. Notably, the values operator only states factors influencing the utility function, not the nature of this relation — agents’ true utility functions are of strict strategic relevance, and no reasonable agent could be persuaded to report them honestly. Instead the declaration serves as a basis for negotiation, that is, by stating what each participant values, agents can propose or counter-propose protocols that others are incentivised to accept. A buyer that fails to declare value on the book invites protocols where it pays and receives nothing. The values declarations establish terms on which protocols are mutually acceptable. Once added, , Vol. 1, No. 1, Article . Publication date: May 2026.
4
Gopinathan et al.
each agent can inject beliefs about other participants’ utilities into the protocol and analyse whether participating is beneficial. 2.3
Capturing Priors over the World
So far, we have extended Pact by making agent decisions and objectives explicit, but one more component is needed to capture the full strategic nature of agentic interactions: prior assumptions about the world also substantially influence how agents reason and act. A buyer that believes books are generally high quality might accept a higher price, while one who does not, will refuse. To capture these additional factors, we extend every protocol with a third participant, the world, whose decisions correspond to exogenous actions, that is, those that must be modelled independently by each participant. In particular, in the book seller protocol, we update the protocol to declare that the quality of the book is a property determined outside of the actions of each participant, book.quality <- world.choose(float). Similar to the value declaration, these serve as a basis for negotiation, and when analysing the game, agents will inject their priors over the world and use them to reason about the expected payoff from participating. 2.4
Pact, a language for protocols with Trust
Putting it all together Figure 2 presents the canonical buyer seller protocol encoded as a Pact protocol. The let bookseller () = book.quality <- world.choose(float) protocol first declares that the quality of the book will be buyer.values(book.quality) modelled as an exogenous variable, and that the buyers send(title, seller) price = seller.choose(float) utility will be dependent on this quality. The protocol send(price, buyer) then proceeds as a traditional choreography, with the if broadcast(buyer.choose(bool)) then exchange( buyer sending the title it wants to the seller. We replace buyer, seller, local computations with strategic relevance with explicit book, price ) choice operators, so in the next step, the seller chooses a price and sends it back to the buyer — each strategic operation is assumed to be made taking into account any Fig. 2. Pact encoding of the full buyer seller and all information that the agent has access to, i.e. in protocol, with explicit agent choices, preferences and priors over the world. this case, the title of the book. The buyer then makes a decision about this price, and broadcasts it to all participants to branch. If the price is accepted, then the exchange concludes and the buyer receives the book, the seller the price. In this way, Pact protocols capture both the communication pattern of a distributed protocol, enough strategic information to encode a formal game. This allows participants to analyse these protocols to answer game theoretic questions of their interactions, such as whether participating in a protocol is beneficial given their assumptions, or as we will demonstrate in the next section, decision policies for their local choices. 3
A decision policy solver for Pact protocols
Pact protocols correspond to formal games, and can be analysed as such. In this section we present an initial such analysis built on top of Pact, implementing a decision policy solver that computes how agents should act given their beliefs about each other. In doing so, we obtain a rather fun result: our canonical choreographic bookseller protocol, treated as a game, allows us to recreate the game theory phenomenon of a Market for Lemons [3], where buyers, uncertain of the quality of the good, must reason through information asymmetry with only access to the price. , Vol. 1, No. 1, Article . Publication date: May 2026.
Pact: A Choreographic Language for Agentic Ecosystems
5
Buyer model world
Seller model
𝑞
seller
seller knows
chooses
𝑞
𝑝
observes
infers
𝑝
𝑞ˆ
ℓ −1
buyer
knows
chooses
𝑞
𝑝
observes
infers
𝑝
𝑞ˆ
buyer
ℓ −1
𝑈
𝑈
𝑞ˆ − 𝑝
ˆ 𝑝 · Pr[𝑞=1]
known
uncertain
utility
cond.
simulates
Fig. 3. Recursive theory-of-mind structure for the buyer-seller protocol. Each agent maintains a generative model of the interaction: Left: the buyer imagines a world that draws book quality, and a seller (dashed frame) who observes it and sets a price; the buyer then conditions on the observed price to infer quality and evaluates utility as inferred quality minus price. Right: the seller knows quality, chooses a price, and simulates a buyer (dashed frame) who observes that price and infers quality; the seller maximises expected revenue weighted by the probability the simulated buyer believes quality is high. Dashed arrows between frames mark recursive calls at depth ℓ−1, bottoming out at ℓ = 0 with naïve priors. Solid frames denote the modelling agent’s own perspective; dashed frames denote simulated counterparts.
3.1
Theory of Mind for Protocols
How should agents make their local decisions in a Pact protocol? What price should the seller set for its books? What price should the buyer make a purchase? The answer to these questions is in some sense inherently recursive. The price the seller should set is the highest price the buyer will accept; the price at which the buyer should accept is the lowest price the seller will set for a high quality good, and so on. Given priors on exogenous variables and utility functions, solving for a decision policy requires modelling other agents’ reasoning, that is, a theory of mind. We implement an analysis based on this observation using the memo programming language [8]. The memo language was developed to aid cognitive science researchers build efficient computational models of theory of mind, providing a concise DSL for expressing such models, and a compiler that reduces them to recursive probabilistic programmes over which inference can be performed efficiently. Figure 3 illustrates such a recursive structure that could be used to model the bookseller protocol. In this model, the buyer (left) makes decisions with a theory of mind by simulating a world and a seller, and conditions on the observed price to make an inference about quality; the seller (right) similarly simulates a buyer and chooses a price that maximises expected revenue. Each party in the interaction recursively simulates the other. Depending on the depth of this analysis, these recursive models themselves contain nested, even smaller recursive models. Our key insight here is that a Pact protocol contains all the information to precisely construct theory-of-mind models, and we use this to build a decision policy solver for Pact games. Figure 4 illustrates a theory-of-mind program constructed purely through an endpoint projection of the buyer-seller pact protocol (cf. 2). The resulting memo program directly mirrors the model described previously. Inside thinks, the buyer simulates its model of the world, with the quality of the book being drawn from its prior and the seller observing the quality and choosing a price according to , Vol. 1, No. 1, Article . Publication date: May 2026.
6
Gopinathan et al.
a recursive model S(level, noise). The buyer conditions on the price it actually observes and infers the probability that the quality is high. This memo program corresponds one-to-one to the original Pact program, world.choose becomes a prior, seller.choose a strategic decision, and send operations delivering the observation to the buyer. Once the model is constructed, we can then run infer- @memo ence over it to obtain a decision policy that can be used def B[q: Quality, p: Prices]( level, noise): to run the protocol — a mapping from observed prices buyer: thinks[ world: given(q in Quality, to a probability of accepting. When we run inference wpp=0.6 if q>100 else 0.4), over this protocol, we are able to recreate aspects of the seller: knows(world.q), seller: chooses(p in Prices, phenomenon of the marketplace for lemons [3]: with a wpp=S[world.q, p]( depth 0 reasoning, the buyer naively assumes that high {level}, {noise})) ] prices strongly signal high quality goods, and accepts buyer: observes[seller.p] is p buyer: chooses(q in Quality, proportional to the price given; the seller recursively rewpp=Pr[world.q == q]) alises this and picks high prices irrespective of the quality return Pr[buyer.q == 1] of the good. As the depth of the recursive reasoning is Fig. 4. Buyer Theory of Mind increased, the acceptance probabilities even out as the buyer becomes more strategic, learning that high prices signal quality, but with diminishing confidence.
4
The Landscape of Multi-Agentic Ecosystems
In this work, we propose extending choreographic languages with operations to encode participants’ preferences and utilities, allowing choreographies to encode not only an executable specification of what agents will do, but also why participants would want to participate. In this way, our formalism bridges from programming languages, to a rich literature from the field of game theory. A number of prior works have investigated the design of DSLs to describe specific classes of formal games. Several DSLs target specification of auction-style games where a seller collects bids from several participants: MIND [23] provides a typed declarative grammar for market design and simulation, CoorERE [15] is a graphical modelling language for auctions and De Jonge and Zhang [9] show that the Game Description Language [17] can encode a broad class of auctionstyle negotiation domains. Beyond auctions, Slice [6] provides a DSL for describing cake-cutting protocols. These works have shown that language design can be used to enforce and guide the designs of games, but each addresses a narrow kind of game, eliding analyses of communication structure or cryptographic tools for protocol enforcement. No prior work provides a unified formal object that autonomous agents can use to reason about an interaction end-to-end. There is a parallel line of work from the multi-agent systems literature that has explored negotiation extensively, but largely in unstructured settings [2]. In contemporary LLM-based multi-agent frameworks [7, 12, 14], agents coordinate through natural language conversation: they debate, persuade, and reach consensus on their interactions through iterative dialogue with each other. This flexibility is appealing but fundamentally insufficient for robust coordination. Natural language agreements are ambiguous, unenforceable, and vulnerable to the very failure modes outlined earlier: sycophancy, prompt injection, and coercion. For trustworthy coordination, the output of negotiation must be a formal object, a protocol specification that can be analysed, verified, and executed with guarantees, both at the substrate-level but also security policies. These claims are supported by existing work on protecting single-agent LLMs from prompt injection attacks [10], where prompts are turned into programs to avoid contamination from untrusted inputs.
, Vol. 1, No. 1, Article . Publication date: May 2026.
Pact: A Choreographic Language for Agentic Ecosystems
5
7
Conclusion & Future Work
In this work we have presented Pact, a choreographic language tailored for the domain of multiagentic coordination, extending choreographies so that agents can not only express their communication patterns, the flow of information through a protocol, but also their decisions, priors and utilities. By making strategic concerns explicit, every Pact protocol corresponds to a formal game, and game-theoretic analyses, such as the theory of mind solver from Section 3, can be implemented as endpoint projections. We have implemented Pact as an embedded DSL within Python on top of the effectful [4] library, using algebraic effects [21] to implement endpoint projection. This work is preliminary, and our next steps are to formalise the semantics of Pact, and prove the correctness of endpoint projection to game-theoretic models. We are also investigating richer analyses that can be built on top of this language, such as incentive compatibility checking, equilibrium computation and automatic mechanism design over Pact protocols by program synthesis. References [1] [n. d.]. Agents Rule of Two: A Practical Approach to AI Agent Security. https://ai.meta.com/blog/practical-ai-agentsecurity/. [2] 2026. Multi-Agent AI Systems Need Transparency. Nature Machine Intelligence 8, 1 (Jan. 2026), 1–1. doi:10.1038/s42256026-01183-2 [3] George A. Akerlof. 1970. The Market for "Lemons": Quality Uncertainty and the Market Mechanism. The Quarterly Journal of Economics 84, 3 (Aug. 1970), 488–500. [4] Basis Research Institute. 2024. Effectful: Algebraic Effects for Python. https://github.com/BasisResearch/effectful https://github.com/BasisResearch/effectful. [5] Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, and Joseph P. Near. 2025. Efficient, Portable, Census-Polymorphic Choreographic Programming. Proc. ACM Program. Lang. 9, PLDI (June 2025), 193:1143–193:1166. doi:10.1145/3729296 [6] Noah Bertram, Alex Levinson, and Justin Hsu. 2023. Cutting the Cake: A Language for Fair Division. Proceedings of the ACM on Programming Languages 7, PLDI (June 2023), 1779–1800. arXiv:2304.04642 [cs] doi:10.1145/3591293 Comment: 31 pages, 15 figures, PLDI 2023. [7] Chi-Min Chan, Weize Chen, Yusheng Su, Jianxuan Yu, Wei Xue, Shanghang Zhang, Jie Fu, and Zhiyuan Liu. 2023. ChatEval: Towards Better LLM-based Evaluators through Multi-Agent Debate. arXiv:2308.07201 [cs] doi:10.48550/ arXiv.2308.07201 [8] Kartik Chandra, Tony Chen, Joshua B. Tenenbaum, and Jonathan Ragan-Kelley. 2025. A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning. Proc. ACM Program. Lang. 9, OOPSLA2 (2025). doi:10.1145/ 3763078 [9] Dave De Jonge and Dongmo Zhang. 2021. GDL as a Unifying Domain Description Language for Declarative Automated Negotiation. Autonomous Agents and Multi-Agent Systems 35, 1 (April 2021), 13. doi:10.1007/s10458-020-09491-6 [10] Edoardo Debenedetti, Ilia Shumailov, Tianqi Fan, Jamie Hayes, Nicholas Carlini, Daniel Fabian, Christoph Kern, Chongyang Shi, Andreas Terzis, and Florian Tramèr. 2025. Defeating prompt injections by design. arXiv preprint arXiv:2503.18813 (2025). [11] Edoardo Debenedetti, Jie Zhang, Mislav Balunovic, Luca Beurer-Kellner, Marc Fischer, and Florian Tramèr. 2024. AgentDojo: A Dynamic Environment to Evaluate Prompt Injection Attacks and Defenses for LLM Agents. In Advances in Neural Information Processing Systems, A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang (Eds.), Vol. 37. Curran Associates, Inc., 82895–82920. doi:10.52202/079017-2636 [12] Yilun Du, Shuang Li, Antonio Torralba, Joshua B Tenenbaum, and Igor Mordatch. 2023. Improving factuality and reasoning in language models through multiagent debate. arXiv preprint arXiv:2305.14325 (2023). [13] Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. 2024. Choral: Object-oriented Choreographic Programming. ACM Transactions on Programming Languages and Systems 46, 1 (March 2024), 1–59. doi:10.1145/3632398 [14] Sirui Hong, Mingchen Zhuge, Jiaqi Chen, Xiawu Zheng, Yuheng Cheng, Ceyao Zhang, Jinlin Wang, Zili Wang, Steven Ka Shing Yau, Zijuan Lin, Liyang Zhou, Chenyu Ran, Lingfeng Xiao, Chenglin Wu, and Jürgen Schmidhuber. 2024. MetaGPT: Meta Programming for A Multi-Agent Collaborative Framework. arXiv:2308.00352 [cs] doi:10.48550/arXiv. 2308.00352 [15] Samaneh Hoseindoost, Afsaneh Fatemi, and Bahman Zamani. 2024. An Executable Domain-Specific Modeling Language for Simulating Organizational Auction-Based Coordination Strategies for Crisis Response. Simulation Modelling Practice and Theory 131 (Feb. 2024), 102880. doi:10.1016/j.simpat.2023.102880 , Vol. 1, No. 1, Article . Publication date: May 2026.
8
Gopinathan et al.
[16] Yupei Liu, Yuqi Jia, Runpeng Geng, Jinyuan Jia, and Neil Zhenqiang Gong. 2024. Formalizing and Benchmarking Prompt Injection Attacks and Defenses. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 1831–1847. https://www.usenix.org/conference/usenixsecurity24/presentation/liu-yupei [17] Nathaniel Love, Timothy Hinrichs, David Haley, Eric Schkufza, Michael Genesereth, and Serra Mall. [n. d.]. General Game Playing: Game Description Language Specification. ([n. d.]). [18] Fabrizio Montesi. 2023. Introduction to Choreographies. Cambridge University Press, Cambridge. doi:10.1017/ 9781108981491 [19] Abhiroop Sarkar and Alejandro Russo. 2024. HasTEE+ : Confidential Cloud Computing and Analytics with Haskell. arXiv:2401.08901 [cs] doi:10.48550/arXiv.2401.08901 [20] Gan Shen, Shun Kashiwa, and Lindsey Kuper. 2023. HasChor: Functional Choreographic Programming for All (Functional Pearl). Proc. ACM Program. Lang. 7, ICFP (Aug. 2023), 207:541–207:565. doi:10.1145/3607849 [21] Gan Shen and Lindsey Kuper. 2024. Toward Verified Library-Level Choreographic Programming with Algebraic Effects. In Proceedings of the International Conference on Choreographic Programming (CP). University of California, Santa Cruz, USA. Pre-print. [22] Manuel Veiga. 2025. Choreographies for Secure Computation. Ph. D. Dissertation. University of Porto. [23] Zhicheng Yang, Li Peihang, Wuqiang Zheng, Zhiyang Dou, Minghao Guo, Benjamin Tod Jones, and Wojciech Matusik. 2025. MIND: Market Interpretation DSL for Unified Market Design and Simulation. (Oct. 2025).
Received 30 March 2026
, Vol. 1, No. 1, Article . Publication date: May 2026.