Fabrizio Montesi
We present an overview of some recent efforts aimed at the development of Choreographic Programming, a programming paradigm for the production of concurrent software that is guaranteed to be correct by construction from global descriptions of communication behaviour.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Choreographic Programming is a programming paradigm for building concurrent programs that are deadlock-free by construction, as a result of programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that explains which computations can be performed with the hallmark constructs of choreographies is still missing. In this work, we introduce Core Choreographies (CC), a model that includes only the core primitives of choreographic programming. Every computable function can be implemented as a…
Corps: A Core Calculus of Hierarchical Choreographic Programming
本文提出层次化编排编程概念，并设计了语言Corps，通过授权逻辑中的命题即类型解释，将数据所有权建模为模态，解决了通信非线性建模与逻辑对应问题。
Choreographic Programming of Isolated Transactions
本文提出一种新的编排编程语言设计，通过跟踪变量使用权限并结合模型检验来证明隔离性，从而支持重叠进程集合间的隔离事务。
HasChor: Functional Choreographic Programming for All (Functional Pearl)
本研究提出一种基于单子的函数式编排编程新模型，支持高阶与位置多态编排特性，并在Haskell库HasChor中实现，让普通Haskell开发者可便捷使用编排编程，且库实现简洁精炼。
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free. Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic …
Choral: Object-Oriented Choreographic Programming
本文提出首个基于主流抽象的编排式编程语言 Choral，通过引入分布式数据类型概念将编排式与面向对象编程相融合，实现了模块化角色代码生成，并凭借对象传递等特性成为首个高阶编排式语言。
Choreographic Programming: a Semantic Approach
本文针对编排式编程中端点投影定理证明困难的问题，通过设计基于进程局部视图的编排新语义及相关预序关系，给出了端点投影定理的模块化证明，使其更简单并增进了对编排式编程理论的理解。
A Promising Future: Omission Failures in Choreographic Programming
针对分布式系统中的发送、接收与网络遗漏故障，提出支持独立恢复策略和投递保证静态检查的编排式编程理论，并在 Choral 中实现验证。
Real-World Choreographic Programming: Full-Duplex Asynchrony and Interoperability
本文首次用编排式编程语言Choral实现IRC协议，验证了该范式在真实世界协议中的可行性，并通过子类型化扩展解决选择通信的静态检测问题，实现与第三方软件的互操作性。
Portable, Efficient, and Practical Library-Level Choreographic Programming
针对库级编排编程在可移植性、效率和实用性上的缺陷，提出EPP-as-DI与编排飞地两项新技术，并在Rust语言的首个CP库ChoRus中实现，显著提升了可用性与性能。
MultiChor: Census Polymorphic Choreographic Programming with Multiply Located Values
针对分布式并发编程的死锁检测与推理难题，提出Haskell库MultiChor，无需额外通信处理选择知识，且支持参与者数量多态的编排表达。
Accompanist: A Runtime for Resilient Choreographic Programming
本文提出Accompanist运行时，通过与可定制运行时协同设计，使编舞编程在去中心化环境下实现鲁棒性，无需修改编译器，支持在现有代码库中部署。
Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. Choreographic programming addresses this challenge by equipping developers with high-level abstractions for codifying the desired communication structures from a global viewpoint. Given a choreography, implementations of the involved processes can be automatically generated by endpoint projection (EPP). While choreographic programming prevents manual mis…
Efficient, Portable, Census-Polymorphic Choreographic Programming
本文针对库级编舞编程的局限，提出conclaves与多重定位值、端点投影作为依赖注入及普查多态三项技术，并在Haskell、Rust和TypeScript中实现，以提升效率与可移植性。
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
针对现有编排语言缺乏节点动态决策计算执行者并传递决策的能力，提出首个具有一等进程名、支持类型与（集合）位置多态的类型化编排语言λ_{QC}，提升表达能力并验证死锁自由等特性。
Toward Verified Library-Level Choreographic Programming with Algebraic Effects
针对库级编排编程缺乏坚实理论基础的问题，提出用代数效应建模该范式的方法，实现了基于Agda的原型框架，并正推进其正确性证明工作。
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these proofs has led to important errors being found in published works. In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of…
Mech: Mechanised Choreographic Programming
研究针对编排编程，提出在Lean 4中的新机械化Mech，解决现有问题。核心方法是制定新语义、揭示代数定律。主要贡献是证明EPP相关特性，推导投影网络相关属性，形成最广泛的CP机械化理论。
Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthesising process implementations automatically. So far, choreographic programming has been explored in the monadic setting: interaction terms express point-to-point communications of a single value. However, real-world systems often rely on interactions of polyadic nature, where multiple values are communicated among two or more parties, like multicast, scatter-gather, and atomic exchanges. We introduce a new model for…
Mechanizing Choreographic Programs and Hoare Logic with State Transformers
该研究将状态变换子模型引入编排编程，在Lean中机械化实现支持多种通信与方法的编排语言，证明了端点投影等性质及霍尔逻辑，规避了绑定替换问题以简化机械化。
On Eliminating the Impossible with Dependent Types: Choreographic Libraries with Proof-Carrying Located Values
本文提出基于依赖类型Lean的编排库ChorLean，通过携带证明的定位值实现完全端点投影，消除部分性问题，支持与MultiChor相同功能。
We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
针对传统编排编程需插入select操作保证通信一致的问题，提出支持多位置值与多播的新型编排语言He-Lambda-Small，通过条件判定值多位置化替代select，类型良好即可保证无死锁，可简洁编码复杂通信模式。
Qoreo: Choreographic Programming for Quantum Distributed Systems
研究针对分布式量子系统编程难题，提出Qoreo语言，它以全局编排表达协议，含局部量子语言等。证明编排类型安全，定义端点投影，其元理论机械化，还提供提取管道用于模拟与部署。
We present AIOCJ, a framework for programming distributed adaptive applications. Applications are programmed using AIOC, a choreographic language suited for expressing patterns of interaction from a global point of view. AIOC allows the programmer to specify which parts of the application can be adapted. Adaptation takes place at runtime by means of rules, which can change during the execution to tackle possibly unforeseen adaptation needs. AIOCJ relies on a solid theory that ensures applications to be deadlock-free by construction also after adaptation. We describe the architecture of AIOCJ, …
Type-Based Enforcement of Non-Interference for Choreographic Programming
本文提出了一种参数化策略类型系统，用于在舞剧编程中强制执行非干扰，防止高安全数据泄露，并通过程序计数器纪律处理显式和隐式流。
Ozone: Fully Out-of-Order Choreographies
针对编排式编程中进程固定顺序执行导致高延迟且乱序易引发通信完整性违规的问题，提出保证无CIVs和死锁的乱序编排模型，并在Choral语言中实现对应API，验证其可降延迟提吞吐。
Reasoning about Choreographic Programs
本文针对编排编程领域其他性质验证研究不足的问题，提出一种Hoare风格的编排行为推理逻辑，证明其可靠性与完备性，且编排的功能正确性性质可传递至编译后的分布式实现。
Step in Tine: Forking Processes in Functional Choreographies
本文提出函数式编舞语言$λ{\pitchfork}$，通过引入进程分叉原语，在保证无死锁的同时支持动态进程创建、任务分配和通信，应用于负载均衡和并行分治等场景。
Towards a Function-as-a-Service Choreographic Programming Language: Examples and Applications
本文提出面向无服务器 FaaS 的编排式编程语言 FaaSChal，通过示例说明投影等特性，并利用编排提取函数基础设施关系以自动生成兼顾用户约束与低延迟的策略。
Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in pa…
Choreographic Programming is a development methodology for concurrent software that guarantees correctness by construction. The key to this paradigm is to disallow mismatched I/O operations in programs, called choreographies, and then mechanically synthesise distributed implementations in terms of standard process models via a mechanism known as EndPoint Projection (EPP). Despite the promise of choreographic programming, there is still a lack of practical evaluations that illustrate the applicability of choreographies to concrete computational problems with standard concurrent solutions. In th…
Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according to the strict control flow described in the choreography, and do not deadlock. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for …
Choreographies as Macros
本文利用Racket的宏系统构建新编舞语言Choret，以简化并发编程中的发送接收配对，避免死锁，并复用基础设施提升功能与正确性。
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. W…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。