Rust: The Programming Language for Safety and Performance
Rust是一种年轻的程序设计语言，自2010年由Mozilla推出以来，它越来越受到软件开发人员的关注。在这项研究中，我们试图回答几个研究问题。Rust是否值得如此多的关注？Rust中有什么吸引程序员使用这种新语言？安全性和性能是Rust最早的承诺之一，正如其早期开发人员所声称的那样。Rust是一种高性能的安全语言吗？这些要求是否已经实现？为了回答这些问题，我们调查和分析了最近关于Rust的研究，以及将Rust与其他可用的著名程序设计语言进行基准测试的研究。结果表明，Rust值得程序员增加兴趣，最近的基准测试研究的实验结果表明，Rust在性能，安全性和安全性方面优于其他成熟的语言。尽管这项研究并不全面（在这一领域还需要做更多的工作），但它向编程和研究社区提供了Rust作为未来语言选择的前景。
2022-06-11 cs.PL cs.SE
The Case for Writing Network Drivers in High-Level Programming Languages
在所有生产级服务器、桌面和移动操作系统上，驱动程序都是用C或C++的受限子集编写的。它们占Linux代码的66%，但2017年在Linux中发现的40个与内存安全相关的安全漏洞中有39个位于驱动程序中。这些错误可以通过为驱动程序使用高级语言来防止。我们展示了使用Rust、Go、C#、Java、OCaml、Haskell、Swift、JavaScript和Python实现的英特尔ixgbe 10 Gbit/s网卡的用户空间驱动程序，这些驱动程序都是以各自语言的惯用风格从头开始编写的。我们量化了使用这些语言的成本和收益：高级语言更安全（错误更少，安全检查更多），但运行时安全检查会降低吞吐量，垃圾回收会导致延迟峰值。乱序CPU降低了安全检查的成本：我们的Rust驱动程序每个数据包执行的指令增加了63%，但只比参考C实现慢4%。Go的垃圾收集器即使在重负载下也能将laptop保持在100 $μ$ s以下。其他语言的情况更糟，但它们独特的属性是一个有趣的案例研究。所有实现都可以在www.example.com上免费获得。
2019-09-13 cs.NI cs.PL
Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types
现代网络编程涉及协调浏览器客户端和服务器之间的交互。通常，基于Web的分布式系统中的交互是非正式描述的，这使得很难确保正确性，特别是通信安全性，即所有端点都没有类型错误或死锁，符合指定的协议。我们提出了STScript，一个工具链，它生成TypeScript API，用于通过WebSockets进行通信安全的Web开发，以及RouST，一种新的会话类型论，支持具有路由机制的多方通信。STScript为开发人员提供了基于RouST的通信协议规范生成的TypeScript API。生成的API建立在TypeScript并发实践的基础上，补充了全栈Web开发中的事件驱动编程风格，并且与服务器端端点的Node.js运行时和浏览器端端点的React.js框架兼容。RouST可以表达通过中间参与者路由的多方交互。它支持浏览器端端点之间的对等通信，通过服务器路由通信，避免过度序列化。RouST保证使用STScript API编写的端点Web应用程序的通信安全。我们使用几个部署为Web应用程序的生产就绪的案例研究来评估STScript对现代Web编程的表现力。
2021-01-12 cs.PL cs.SE
Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)
这项工作介绍了新的概念，细化，我们开发的上下文中明确多态ML类语言与类型级计算。正如类型精化通过类型域中的值上的谓词所表达的理解原则来嵌入丰富的规范一样，种类精化通过种类域中的类型上的谓词来提供丰富的种类规范。通过利用我们强大的细化类规则，我们语言中的类型不仅用于静态地对程序表达式和值进行分类，而且还可以方便地作为树状数据结构进行操作，并通过对此类结构的逻辑约束来细化它们的类。值得注意的是，由此产生的类型和分类规则允许强大的类型反射，ad-hoc多态和类型元编程，这些通常在现代软件开发中发现，但通常不能在通用语言中以类型安全的方式表达。我们通过建立类型安全的标准元理论结果，并通过一个原型实现的一种检查器，类型检查器和解释器，我们的语言，验证我们的方法在形式上和实用。
2019-08-01 cs.PL
LoRe: A Programming Model for Verifiably Safe Local-First Software
针对本地优先软件缺乏自动化安全保证的问题，本文提出 LoRe 编程模型与编译器，结合响应式编程、静态分析和验证来识别不安全并发交互并按需引入协调一致性。
2023-10-19 cs.PL
Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
University of Kent（肯特大学）；Utrecht University（乌得勒支大学）；Tweag
本研究在纯函数式编程中形式化和实现了安全的目标传递，通过设计灵活的类型系统确保安全性，并在Haskell中验证了其可行性。
2026-01-13 cs.PL
Qimaera: Type-safe (Variational) Quantum Programming in Idris
变分量子算法是经典-量子混合算法，其中经典和量子计算协同工作以解决计算问题。这些算法为设计合适的程序设计语言带来了有趣的挑战。在本文中，我们介绍Qimaera，这是一组库的Idris 2程序设计语言，使程序员实现（变分）量子算法的优雅的Idris语言的全部力量与量子编程原语，我们介绍同步工作。Idris的两个关键要素使这成为可能：（1）依赖类型，允许我们实现幺正（即可逆和可控）量子操作;（2）线性，允许我们对量子操作的执行进行细粒度控制，确保遵守量子力学定律。我们证明了Qimaera是适合变分量子编程提供实现的两个最突出的变分量子算法- QAOA和VQE。据我们所知，这是这些算法在类型安全框架中的第一个实现。
2021-11-21 cs.LO cs.PL quant-ph
Type Safe Redis Queries: A Case Study of Type-Level Programming in Haskell
Redis是一种内存中的数据结构存储，通常用作数据库，具有Haskell接口Hedis。Redis是动态类型的--一个键可以被丢弃并重新关联到一个不同类型的值，当一个命令获取一个它不期望的类型的值时，它会发出一个运行时错误的信号。我们开发了一种特定于域的语言，通过利用Haskell的类型级编程技术，包括索引monad，类型级字面量和封闭类型家族，跟踪数据库中的值类型，并静态地保证一类Redis程序不会发生类型错误。
2017-08-30 cs.PL
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
几乎每一种编程语言的语法都包含绑定器和相应的绑定事件的概念，以及伴随的$α$等价、避免捕获的替换、类型上下文、运行时环境等概念。在过去，实现和推理程序设计语言需要仔细处理以维护绑定变量的正确行为。现代程序设计语言包含了一些特性，这些特性使得像范围安全这样的约束可以用类型来表达。尽管如此，程序员仍然被迫为范围安全操作的每个新实现重新编写相同的样板（例如，重命名、取代、脱糖、印刷等），然后再进行正确性证明。我们提出了一个具有约束力的语法表达宇宙，并演示了如何（1）实现范围安全遍历一劳永逸的泛型编程;（2）如何派生这些遍历的属性泛型证明。我们的宇宙描述，一般的遍历和证明，以及我们的例子都已经在Agda中正式化，并且可以在https://github.com/gallais/generic-syntax在线获得的附带材料中获得。
2021-10-12 cs.PL
Fencing off Go: Liveness and Safety for Channel-based Programming (extended version)
Go是一种生产级静态类型的程序设计语言，其设计特点是显式的消息传递原语和轻量级线程，使（并鼓励）程序员能够开发并发系统，其中组件通过通信进行交互，而不是基于锁的共享内存并发。Go语言只能在运行时检测全局死锁，但不能提供编译时保护来防止所有常见的通信不匹配或部分死锁。这项工作开发了一个静态验证框架，在Go程序的活性和安全性，能够检测通信错误和部分死锁在一般类的现实并发程序，包括那些与动态通道创建，无限线程创建和递归。我们的方法从Go程序中推断出其通信模式作为行为类型的忠实表示。通过检查通道使用的语法限制，被称为围栏，我们确保程序是由许多不同的通信模式，可以重复无限多次。这个限制允许我们实现过程来检查类型中的活性和安全性，这反过来又近似于Go程序中的活性和安全性。我们已经在一个工具链中实现了类型推断、活性和安全检查，并在公开的Go程序中进行了测试。注：这是POPL 2017中发表的一篇论文的修订扩展版本，详情请参见第13页。
2017-02-28 cs.LO cs.PL
Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types
通信系统包括跨网络的各种软件组件。为了确保它们的鲁棒性，现代程序设计语言（如Rust）提供了强类型通道（其使用保证是仿射的（最多一次））和二进制通道上的取消操作。为了协调组件正确地相互通信和同步，我们使用多方会话类型的结构化机制，用仿射通信信道和隐式/显式取消机制对其进行扩展。这种新的类型规则，仿射多方会话类型（AMPST），确保取消终止多个独立运行的组件，并保证通信不会由于错误或突然终止而卡住。在AMPST的指导下，我们实现了一个与取消终止算法相关的Rust API自动生成工具（MultiCrusty），Rust编译器通过该工具自动检测不安全的程序。我们的评估表明，MultiCrusty提供了一种有效的机制，用于通信，同步和传播任意进程的取消通知。我们已经实现了几个用例，包括流行的应用程序协议（OAuth，SMTP）和具有异常处理模式的协议（断路器，分布式日志记录）。
2022-04-28 cs.PL
Session-Based Programming for Parallel Algorithms: Expressiveness and Performance
本文研究会话编程和类型的基准测试的例子，比较生产力，安全性和性能与其他通信程序设计语言。并行算法被用来检查上述方面，由于它们广泛使用的消息传递的交互，以及它们在算法研究中的日益突出的硬件资源，如多核机器和集群的可用性。我们贡献了新的基准测试结果SJ，Java的类型安全，二进制会话编程的扩展，对MPJ Express，基于MPI标准的Java消息传递系统。总之，我们观察到（1）尽管有丰富的库和功能，MPI仍然是一个低级API，并且可能遭受显式消息传递的常见缺点，如死锁和意外的消息类型，以及（2）高级会话抽象的好处，这对程序结构有显着影响，以提高可读性和可靠性，并且会话类型安全可以极大地促进通信编程的任务，同时保持有竞争力的性能。
2010-02-04 cs.DC cs.PL
Gemini: A Functional Programming Language for Hardware Description
本文介绍了双子座，功能程序设计语言的硬件描述，提供的功能，如参数多态性，递归数据库，高阶函数，和类型推断更高的表达能力相比，现代硬件描述语言。Gemini通过其独特的类型系统（由多个原子类型和依赖类型组成）演示了新颖的类型理论概念的理论和实现，该类型系统允许该语言安全地对软件和硬件构造进行建模，并通过多阶段编译执行类型推断。本文的主要技术成果包括形式化的双子座语法，类型规则，和评估规则，双子座的类型系统的安全性证明，和编译器的语义分析阶段的原型实现。
2019-11-10 cs.PL
SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems
University of California at Berkeley, CA, USA（加州大学伯克利分校）；SRI International（SRI国际）；Microsoft（微软）
本文提出SOTER框架，通过一种编程语言和集成的运行时保证系统，为安全机器人系统提供保障，确保在使用未经认证组件时仍能满足安全要求。
2019-04-19 cs.AI cs.PL cs.RO
Obsidian: Typestate and Assets for Safer Blockchain Programming
区块链平台正在广泛用于处理尚未建立相互信任的参与者之间的关键交易。许多区块链都是可编程的，支持智能合约，智能合约维护持久状态并支持转换状态的交易。不幸的是，许多智能合约中的漏洞已经被黑客利用。Obsidian是一种新颖的程序设计语言，它的类型系统可以静态检测当今智能合约中常见的错误。黑曜石是基于一个核心演算，二氧化硅，我们证明了类型的可靠性。Obsidian使用typestate来检测不适当的状态操纵，使用线性类型来检测资产滥用。我们描述了两个案例研究，评估黑曜石的适用性的领域的参数保险和供应链管理，发现黑曜石的类型系统有利于推理高层次的国家和所有权的资源。我们将我们的Obsidian实现与Solidity实现进行了比较，观察到Solidity实现需要大量的样板检查和状态跟踪，而Obsidian静态地完成这项工作。
2019-09-08 cs.PL cs.SE
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2
Rust程序设计语言作为一种现代的、类型安全的、内存安全的、潜在的可形式化分析的程序设计语言，已经引起了人们的极大兴趣和使用。我们对Rust的兴趣源于它作为硬件/软件共同保证语言的潜力，并应用于自动驾驶汽车等关键系统。我们报告了Rust作为高级合成（HLS）语言的首次使用。大多数现有的HLS语言都是C的子集。基于Rust的HLS为硬件和软件实现带来了一种现代的、类型安全的、内存安全的表达式语言，具有很高的保证。为了研究Rust作为HLS的适用性，我们精心制作了一个Rust子集，灵感来自Russinoff的Restricted Rummic C（RAC），我们将其命名为Restricted Rummic Rust或RAR。在我们的第一个RAR工具链实现中，我们简单地将RAR源代码转换为RAC。通过这样做，我们利用了一些现有的硬件/软件共同保证工具，以最少的时间和精力投资。在本文中，我们描述了RAR Rust子集，详细介绍了我们的原型RAR工具链，并描述了实现和验证的几个代表性的算法和数据结构编写的RAR，使用ACL 2定理证明进行的正确性证明。
2022-05-24 cs.LO cs.PL
Speak Now: Safe Actor Programming with Multiparty Session Types (Extended Version)
University of Glasgow（格拉斯哥大学）；Queen Mary University of London（伦敦大学女王玛丽学院）
Maty是首个支持静态多方会话类型和多会话Actor的编程语言，通过流敏感效果系统和事件驱动编程实现通信安全与系统容错。
2026-03-03 cs.PL
Toka: A Systems Programming Language with Explicit Resource Semantics
USTC（中国科学技术大学）
提出一种名为Toka的系统编程语言，通过显式资源语义（Handle-Soul对偶模型）在语法层面分离指针标识与值，从而在保持物理透明性的同时实现编译时内存安全，并降低生命周期标注的认知负担。
2026-06-01 cs.PL
Safe Stream-Based Programming with Refinement Types
在基于流的编程中，数据源被抽象为可以通过回调函数操作的值流。基于流的编程正在迅速流行，因为它为交互式软件中处理异步数据源提供了一个强大的和富有表现力的范例。但是，高级流抽象也会使开发人员难以推理程序中的控制流和数据流关系。这在异步流代码与线程受限功能（例如将UI访问限制为单个线程的UI框架）交互时特别有影响，因为流结构的线程行为通常是不直观的，并且没有充分的文档记录。在本文中，我们提出了一个基于类型的方法，可以静态地证明线程安全的UI访问流为基础的软件。我们的关键见解是，流处理框架的流畅API支持通过类型细化跟踪线程，从而可以自动推断代码在哪个线程上运行-这通常是一个难题。我们将该系统实现为基于注释的Java typechecker，用于基于流行的ReactiveX框架构建的Android程序，并通过注释和分析8个开源应用程序来评估其功效，在这些应用程序中，我们发现33个不安全的UI访问实例，而每186行源代码中只有一个注释的注释负担。我们还报告了将类型检查器应用于Uber Technologies Inc.的两个更大的应用程序的经验。代码库，它目前在每个代码更改时运行，并阻止引入潜在线程错误的更改。
2018-08-09 cs.PL cs.SE
Catroid: A Mobile Visual Programming System for Children
Catroid是一个免费开源的可视化程序设计语言、编程环境、图像处理程序和网站。Catroid允许8岁以上的临时用户和首次用户仅使用Android手机或平板电脑开发自己的动画和游戏。Catroid还允许通过蓝牙无线控制外部硬件，如Lego Mindstorms机器人，蓝牙Arduino板，以及Parrot的流行和廉价的AR.Drone四轴飞行器。
2012-04-28 cs.CY cs.HC cs.PL
What can the programming language Rust do for astrophysics?
天体物理学界使用不同的工具来完成计算任务，如复杂系统模拟、辐射转移计算或大数据。编程语言如Fortran、C或C++通常出现在这些工具中，通常，语言的选择是基于性能的需要。但这是有代价的：安全。例如，一个常见的错误来源是对无效内存区域的访问，这会产生随机执行行为并影响结果的科学解释。2015年，Mozilla Research发布了名为Rust的新编程语言的第一个稳定版本。许多特性使这种新语言对科学界具有吸引力，它是开源的，在提供零成本抽象的同时保证内存安全。我们通过重新实现Mercury-T的基本部分来探索Rust用于天体物理学的优点和缺点，Mercury-T是一种模拟多行星系统的动力学和潮汐演化的Fortran代码。
2017-02-09 astro-ph.IM cs.PL
