logo
科言猫学术研究的AI总结
language
手机端手机端
  • Phone Feature微信小程序
简体中文简体中文
notice消息通知
博客博客
delete
arrow
返回

Choreographic Quick Changes: First-Class Location (Set) Polymorphism

delete2025-10-01
delete0
PRE
AI
A
A.G. Samuelson *
A
Andrew K. Hirsch
E
Ethan Cecchetti
DOI：10.1145/3763114delete
delete原文链接
delete原文求助
delete分享
delete收藏
摘要

摘要

En 中文
编排式编程是一种有前景的新范式，用于编程并发系统，其中开发者编写一个集中的单一程序，该程序编译为每个节点的独立程序。然而，现有的编排式编程语言缺乏现代系统所需的关键特性，例如一个节点动态计算应由谁执行计算并将该决策发送给其他节点的能力。本研究通过lambda QC填补了这一空白，它是第一种具有一等进程名以及对类型和（位置集合）进行多态支持的类型化编排式编程语言。lambda QC还通过支持代数和递归数据类型以及多位置值来增强表达能力。我们在Rocq中形式化并机械验证了我们的结果，包括编排式编程的标准保证——无死锁。
Keyword:
Concurrency
Choreographies
Functional programming

期刊

P
Proceedings of the ACM on Programming Languages-PACMPL
IF:
2.8
论文数:
308
被引数:
4.7K

机构

U
university of wisconsin madison
学者数:
3.8W
论文数: 2.9W
被引数: 53
University of Wisconsin System 封面图
University of Wisconsin System
学者数:
6.7W
论文数: 5.8W
被引数: 382
引用论文

引用论文

Communications in choreographies, revisited
errProceedings of the 33rd Annual ACM Symposium on Applied Computing
IF0
err2018-04-09
err0
PREAI
errCruz-Filipe,Luís; Montesi,Fabrizio; Peressotti,Marco
err分享
err收藏
Introduction to Choreographies编排概论
err
IF0
err2023-05-11
err0
PREAI
errFabrizio Montesi
err分享
err收藏
err
IF0
err
err0
PREAI
err
err分享
err收藏
Alice or Bob?: Process polymorphism in choreographies
errJournal of Functional Programming
IF0
err2024-01-01
err0
PREAI
errGRAVERSEN,EVA; HIRSCH,ANDREW K.; MONTESI,FABRIZIO
err分享
err收藏
Deadlock-freedom-by-design
errProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
IF0
err2013-01-23
err0
PREAI
errMarco Carbone; Fabrizio Montesi
err分享
err收藏
Amending Choreographies修改编舞
errElectronic Proceedings in Theoretical Computer Science
IF0
err2013-07-31
err0
errOAAI
errIvan Lanese; Fabrizio Montesi; Gianluigi Zavattaro
err分享
err收藏
Functional Choreographic Programming
errLecture Notes in Computer Science
IF0
err2022-01-01
err0
PREAI
errCruz-Filipe,Luís; Graversen,Eva; Lugović,Lovro; Montesi,Fabrizio; Peressotti,Marco
err分享
err收藏
Multiparty GV: functional multiparty session types with certified deadlock freedom
errProceedings of the ACM on Programming Languages
IF0
err2022-08-29
err0
PREAI
errJacobs,Jules; Balzer,Stephanie; Krebbers,Robbert
err分享
err收藏
Refinement types for ML
errProceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation - PLDI '91
IF0
err1991-01-01
err0
errOAAI
errTim Freeman; Frank Pfenning
err分享
err收藏
Certifying Choreography Compilation
errLecture Notes in Computer Science
IF0
err2021-01-01
err0
PREAI
errCruz-Filipe,Luís; Montesi,Fabrizio; Peressotti,Marco
err分享
err收藏
学者 查看更多内容