论文

Flambda 2 是一个以内联为中心的 OCaml IR 和优化过程。我们讨论了塑造它的工程约束以及允许编译器足够快以处理非常大的工业代码库的整体结构。

在本演讲中，我们将概述驱动 OCaml 程序 Flambda 2 优化器的抽象域。与大多数优化编译器一样，Flambda 2 依赖于静态分析来查找优化机会。实际上执行了若干不同的分析。在这里，我们将重点关注我们称为 Flambda 2 类型的正向值分析。尽管它的名称如此，但它非常适合抽象域的定义（在抽象解释的意义上），并且我们将通过这个角度来介绍它。

在本演示文稿中，我们将探讨垃圾收集语言（如 Java 或 OCaml）到 WebAssembly (Wasm) 的编译。JavaScript 作为 Web 默认语言的局限性导致了 Wasm 的开发，Wasm 是一种安全且性能可预测的模块化语言。但是，将垃圾收集语言编译到 Wasm 会带来挑战，包括需要编译或重新实现运行时以及在传输已验证属性方面存在的困难。讨论了在内存中表示值的各种技术，重点介绍了 OCaml 的方法。引入了名为 Wasm-GC 的扩展，通过合并 `int31` 和垃圾收集结构等功能，使垃圾收集语言能够编译到 Wasm。本文介绍了 Wasocaml，这是一个完整的 OCaml 到 Wasm-GC 的编译器，并讨论了基准测试和将来将垃圾收集语言编译到 WebAssembly 的工作。

Opam 1.2 于 2014 年发布。在 opam 2.0 取代它之前，它存在了四年，之后 opam 2.1 又存在了三年。Opam 2.2 的发布迫在眉睫，它将在其前身发布一年后问世。本次演讲介绍了添加到 opam 2.1 中的功能，旨在简化处理多个 opam 版本的过程。我们将了解如何存储在“.opam”根目录中以及添加到 opam 命令行中的少量额外元数据，为 opam 的开发人员提供了更轻松地添加新功能的机会，并确信用户能够安全地升级。在介绍这些内容时，我们还将宣传我们认为 opam 2.1（和 2.2）中的一些惊人新功能，以及我们为什么认为您应该密切关注新版本并在发布后立即升级！

用户定义的效应和效应处理程序被宣传和提倡为一种相对易于理解且模块化的分隔控制方法。它们提供了挂起和恢复计算的能力，并允许在请求特定服务的计算与提供此服务的处理程序之间双向传输信息。然而，一个关键问题至今在很大程度上仍未得到解答：在存在用户定义的效应处理程序和原始效应（例如堆分配的可变状态）的情况下，如何以模块化的方式指定和验证程序？我们通过提出一个内置支持效应处理程序（浅层和深层）的分离逻辑来回答这个问题。程序片段的规范包括一个协议，该协议描述了程序可能执行的效应以及它可以预期接收到的回复。该逻辑允许通过框架规则和绑定规则进行局部推理。它基于 Iris 并继承了其所有高级特性，包括对高阶函数、用户定义的幽灵状态和不变式的支持。我们通过几个案例研究来说明其强大功能，包括（1）控制反转的通用公式，它将“推送”元素到消费者的生产者转换为可以按需“拉取”元素的生产者，以及（2）一个简单的协作并发系统，其中多个线程并发执行，可以生成新线程，并通过承诺进行通信。

在本演讲中，我们将介绍一个名为 digodoc 的新工具，该工具构建了 opam 交换的图形，将文件、库和 opam 包关联到包含和依赖项的循环图中。然后，我们将解释如何使用该工具构建一个文档网站，该网站显示来自官方 opam 存储库的大量 opam 包生成的文档。借助 digodoc，用户可以轻松地在模块文档、源代码、包和库之间导航。我们认为这对 OCaml 生态系统来说是一个有趣的贡献。

我们使用 Cosmo（一种现代并发分离逻辑）来正式指定和验证在 Multicore OCaml 弱内存模型设置下实现的多生产者多消费者并发队列。我们将此结果视为 Cosmo 如何允许对高级并发数据结构进行模块化和形式化推理的演示和实验验证。特别是，我们展示了逻辑原子三元组和 Cosmo 的视图的联合使用如何能够在规范中精确地描述队列库与弱内存模型之间的交互。

效应处理程序作为一种用于使用户定义效应进行模块化编程的机制，正获得越来越多的关注。效应处理程序允许以可组合的方式表达非局部控制流机制，例如生成器、async/await、轻量级线程和协程。我们提出了一种设计，并评估了针对 OCaml（一种工业级多范式编程语言）的效应处理程序的完整高效实现。我们的实现力求保持现有 OCaml 代码的反向兼容性和性能特征。将效应处理程序移植到 OCaml 上具有挑战性，因为 OCaml 目前没有任何非局部控制流机制，除了异常之外。我们针对 OCaml 的效应处理程序实现：（i）在不使用效应处理程序的综合宏基准套件上施加了平均 1% 的开销；（ii）与检查堆栈的程序分析工具保持兼容；以及（iii）对于使用效应处理程序的新代码来说是高效的。

在本演讲中，我们将介绍 `opam-bin`，这是一个 opam 插件，可以即时构建二进制 opam 包以加快包的重新安装速度。`opam-bin` 还会为这些二进制包创建 opam 仓库，以便于与其他用户共享。我们将展示它的工作原理以及如何在日常使用中应用它。

在本演讲中，我们介绍了我们使用语法定义形式 SDF3 对 OCaml 语言进行语法定义的工作。SDF3 通过声明式消歧和构造函数定义支持对具体语法和抽象语法的定义，从而能够直接映射到抽象语法。基于 SDF3 语法定义，Spoofax 语言工作台生成一个完整的语法感知编辑器，包括解析器、语法检查、解析错误恢复、语法高亮、带正确括号插入的格式化以及语法补全。语法定义应该为 OCaml 设计和进一步工具开发的实验提供良好的基础。在演讲中，我们将重点介绍语法定义的有趣方面，讨论我们在 OCaml 语法中遇到的问题，并演示编辑器。

自从状态机框架出现以来，它们就证明了自身的价值，从沃尔沃汽车的基础 AUTOSAR 组件到数字发票系统，都发现了缺陷。这些案例研究都是使用 Erlang 的商业 QuickCheck 状态机框架（来自 Quviq）进行的，但现在此类框架也适用于 Haskell、F#、Scala、Elixir、Java 等。我们展示了一个基于 QCheck 库的 OCaml 类型化状态机框架，并说明了所有此类框架中常见的几个概念：状态建模、命令、解释命令、先决条件和一致性检查。

AD-OCaml 是一个库框架，用于通过算法微分计算几乎任意 OCaml 程序的数学精确导数和深度幂级数近似。与类似的框架不同，这包括带有副作用、别名以及嵌套导数运算符的程序。该框架还提供用户程序及其转换的隐式并行化。演示文稿将简要介绍数学问题、实现解决方案的难点、库的设计以及演示其功能。

在本演讲中，我们描述了我们在使用专门用于更改 OCaml 函数签名的自动 API 迁移策略的经验，使用 OCaml 的 Rotor 重构工具。我们使用 Rotor 对开源 Jane Street 库进行案例研究，以重构比较函数，使其返回更精确的变体类型而不是整数。我们讨论了重构 Jane Street 代码库的难点，该代码库广泛使用 PPX 宏，以及正在进行的实现新重构的工作。

多核 OCaml 通过支持共享内存并发扩展了 OCaml。它配备了一个弱内存模型，为此已发布了一个操作语义。这就引出了一个问题：在编写或验证多核 OCaml 代码时，可以依赖哪些推理规则？为了回答这个问题，我们将 Iris（并发分离逻辑的现代后裔）实例化为多核 OCaml。这产生了一种低级程序逻辑，其推理规则揭示了内存模型的细节。在此基础上，我们构建了一个更高级别的逻辑 Cosmo，它以牺牲一些表达能力为代价，换取了一组简单的推理规则，这些规则允许以无数据竞争的方式访问非原子位置，利用原子位置的顺序一致行为，以及利用原子位置的释放/获取行为。Cosmo 允许低级推理（其中多核 OCaml 内存模型的细节是明显的）和高级推理（与该内存模型无关）。我们通过一些案例研究来说明这一点：我们根据经典的、与内存模型无关的规范验证了几种锁的实现。因此，使用锁作为唯一同步手段的粗粒度应用程序可以在 Cosmo 的并发分离逻辑片段中进行验证，而无需任何关于弱内存模型的知识。

Irmin 是一个 OCaml 库，用于构建具有与 Git 相同设计原则的分布式数据库。现有的 Git 用户会发现许多熟悉的功能：分支/合并、所有更改的不可变因果历史以及恢复到任何先前状态的能力。Irmin v2 为存储添加了新的访问方法：我们现在可以从 CLI 或使用 `irmin-graphql` 在浏览器中使用 Irmin。它还有一个新的后端 `irmin-pack`，它针对空间使用进行了优化，并被 Tezos 区块链使用。

LexiFi 维护一个 OCaml 编译器扩展，该扩展通过运行时类型表示启用内省。最近，我们实现了一个语法扩展 (PPX)，它允许在普通编译器上使用 LexiFi 运行时类型。我们建议介绍我们公开可用的运行时类型及其功能。最值得注意的是，我们希望介绍一种使用带孔的运行时类型进行模式匹配的机制。

SmartPy 是一个完整的系统，用于为 Tezos 区块链开发智能合约。它是 Python 中一个嵌入式 EDSL，用于编写合约及其测试场景。它包括一个在线 IDE、一个链浏览器和一个命令行界面。Python 用于生成一种称为 SmartML 的命令式、类型推断的中间语言的程序。SmartML 也是 OCaml 库的名称，该库提供解释器、编译器到 Michelson（Tezos 的智能合约语言）以及场景“链上”解释器。IDE 使用 OCaml 与 `js_of_ocaml` 以及纯 Javascript 的混合构建。命令行界面也使用 `js_of_ocaml` 构建以在 Node.js 上运行。

OCaml-CI 是一个用于 OCaml 项目的 CI 服务。它使用项目 opam 和 `dune` 文件中的元数据来确定要构建的内容，并使用缓存使构建速度更快。它会自动针对多个 OCaml 版本和操作系统平台测试项目。到目前为止，CI 已部署在 GitHub 上的约 50 个项目中，其中许多项目的响应时间比集成度较低的 CI 解决方案快一个数量级。本演讲将介绍 CI 服务，然后介绍用于构建它的某些技术。

随着最近 OCaml 版本（4.10 和 4.11）的多核变体的可用性，这些变体与现有的 OCaml C-API 保持向后兼容，更广泛的 OCaml 社区对并行化现有 OCaml 代码的兴趣越来越大。

OCaml 是一种工业级、多范式编程语言，广泛应用于工业界和学术界。OCaml 也是为数不多的现代托管系统编程语言之一，缺乏对共享内存并行编程的支持。本文描述了 OCaml 编程语言多核扩展的大部分并发垃圾回收器 (GC) 的设计、完整实现和评估。鉴于我们建议为一种拥有数百万行现有代码的广泛使用的编程语言添加并行性，我们面临着保持向后兼容性的挑战——不仅在语言功能方面，而且在使用新 GC 运行的单线程代码的性能方面也是如此。为此，本文提出了一系列新技术，并证明了新的 GC 在顺序程序的性能和功能向后兼容性之间取得了平衡，并且在现代多核处理器上具有出色的扩展性。

`odoc` 是最新尝试创建的文档工具，它旨在处理 OCaml 语言的全部复杂性。这个项目酝酿已久，因为同时处理模块系统和生成富文本文档是一项艰巨的任务。尽管如此，我们相信最近的两项发展为 OCaml 文档难题提供了最后的拼图。这两项改进将 `odoc` 分成了两层：模型层，深入理解模块系统；文档层，方便定义新的输出格式。

本提案描述了将在 OCaml’20 研讨会上进行的演示。演示将介绍一个新的 OCaml 文件系统 ImpFS 及其相关的库。该文件系统利用了在 OCaml’17 上展示的 B 树库和在 ML’19 上展示的键值存储。此外，还有一些其他支持库可能会引起社区的兴趣。ImpFS 代表了文件系统设计空间中的一个点，但我们希望我们开发的库能够让其他人构建具有新功能的更多文件系统。

Coda 是一种新的加密货币，它使用 zk-SNARKs 来显著减少运行其协议的节点所需的数据量。节点使用从 OCaml 源文件中的类型定义自动派生的格式进行通信。随着 Coda 软件的演进，这些发送数据的格式可能会发生变化。我们希望允许运行旧版软件的节点与新版软件通信。为了实现这一点，我们识别出必须随时间保持稳定的类型，以便它们的序列化也不发生变化。

在本文中，我们分享了在 OCaml 中对化学信息学和结构生物信息学软件进行原型设计的经验。

我们建议对 OCaml 的 `open` 结构进行和谐的扩展。OCaml 现有的结构 `open M` 将模块 `M` 导出的名称导入到当前作用域中。目前，`M` 必须是模块的路径。我们建议扩展 `open` 以接受任意模块表达式，从而能够简洁地解决在编写 OCaml 程序时出现的一些现有的与作用域相关的难题。

我们提出了一种新的共享内存并行程序语义，即使在存在数据竞争的情况下也能提供强大的保证。我们的局部数据竞争自由属性保证程序的所有无数据竞争部分都表现出顺序语义。我们提供了一个简单的操作语义和一个等价的公理化模型，并评估了 OCaml 编程语言的实现。我们的评估表明，在主流编程语言中，可以在易于理解的内存模型与合理的（x86 上无开销，ARM 上约 0.6%）顺序性能权衡之间取得平衡。

我们为 OCaml 提出了一个内存模型，总体上遵循 C++ 和 Java 等语言的公理化内存模型的设计，但有一些差异，以便为程序员提供更强的保证和更简单的推理，但代价是不允许所有可能的优化。

Eff 语言是一种类似 OCaml 的语言，作为代数效应理论的原型实现，旨在大规模地实验代数效应。我们介绍了 Eff 嵌入到 OCaml 中的方法，使用分隔延续库或多核 OCaml 分支。我们使用基于无类型最终风格解释器的表示语义证明了嵌入的正确性，包括多提示分隔控制的新颖的直接表示语义。嵌入是系统的、轻量级的、高效的，甚至支持更高阶的“动态”效应及其多态性。因此，OCaml 可以被视为 Eff 的另一种实现，拓宽了该语言的范围和吸引力。

我们介绍了 Learn OCaml，这是一个 Web 应用程序，它包含一组学习活动，供希望学习 OCaml 的人使用。它包括经过重新设计和集成的久负盛名的 Try OCaml 版本，以及一个来自 OCaml MOOC 开发的、具有自动评分功能的练习环境。它完全在浏览器中运行，服务器用于存储静态文件并在不同设备之间同步。我们特别努力使其在平板电脑甚至手机上可用。一个主要的公共实例将托管在 OCamlPro 上，但该项目是开源的，大学可以在本地托管自己的版本。我们还将提供一个公共存储库，供教师贡献课程和练习。

Louis Gesbert 涵盖了 2016 年 9 月 OCaml 平台的当前状态。介绍了对 opam 2.0 的改变游戏规则的集成、路线图以及 OCaml 平台作为一个整体的许多其他方面，例如 `opam-publish`。

我们介绍了 OCamlPro 的一个正在进行的项目，即基于抽象解释技术的 OCaml 代码语义分析器的开发。此分析依赖于编译时存在整个程序，它应该在完整的实际程序上工作，并在未捕获异常检测方面显示出有趣的希望。

在本演讲中，我们将介绍 OCamlPro 的一个启动项目，即基于 LLDB 调试器（一个构建在 LLVM 框架之上的调试器）的 OCaml 原生代码应用程序调试框架的开发。我们实现了 OCaml 的 LLDB C++ API 的完整绑定，然后使用它构建了几个工具，一个“通用”调试器和两个用于监视 OCaml 应用程序内存行为的小型实用程序。

我们介绍了一个关于向 OCaml 添加命名空间的正在进行的工作。受 Scala 或 C++ 等其他语言的启发，我们的目标是设计和形式化一个简单且非侵入式的命名空间机制，而不会使核心语言复杂化。在我们方法中，命名空间是定义库的简单方法，同时避免名称冲突。它们还旨在简化构建过程，明确并减少（在可能的情况下减少到零）外部工具的责任。

OCaml 平台将 OCaml 编译器工具链与一组用于构建、文档、测试和 IDE 集成的连贯工具结合在一起。该项目是整个 OCaml 社区的协作努力，由剑桥的 OCaml Labs 小组与上面列出的其他主要贡献者紧密联系在一起。平台的需求正在受到工业 OCaml 联盟（主要是 Jane Street、Citrix 和 Lexifi）的指导。本次演讲是对 2013 年 OCaml 演讲的后续，该演讲介绍了该平台。从那时起，许多工具已通过 opam 包管理器并行发布，今年的演讲将演示将它们联系在一起的具体工作流程（见图 2）。我们将首先简要回顾平台的理念，更新 opam 包管理器 v1.2，并以平台工作流程结束。

我花了很多时间修改 OCaml 编译器。因此，当我编写一些代码时，我对生成的汇编代码的样子有一个很好的了解。当我想编写对性能敏感的代码时，这很好，但是因为我通常编写执行时间并不重要的代码，所以这主要让我感到痛苦。我脑海中有一个微弱的声音告诉我“你不应该那样写，你知道你可以避免这种分配。”通常，遵循这种指示只会使代码的可读性降低。但是有一个解决办法可以平息这个声音：让编译器比我聪明。OCaml 编译机制非常可预测。没有黑魔法可以将你的丑陋代码替换为表现良好的代码，但它始终生成合理有效的代码。这通常是一件好事，因为你不会对代码运行速度比你通常期望的慢感到惊讶。但它对愚蠢的代码处理得并不好。对于人类编写的代码，这可能并不经常是一个问题，但生成的代码（例如来自 camlp4/ppx 的代码，或从另一种语言编译到 OCaml 的代码）可能会属于此类。事实上，非人类编写的代码还有另一个常见来源：内联。

OCamlot 为 opam 包的质量和兼容性提供了一个分布式的持续测试服务。OCamlot 使用来自 GitHub 的信号，确保在合并之前，提交到 opam 存储库的补丁在各种支持的配置、架构和系统上进行了彻底的测试。由此产生的构建和元数据质量的提高反过来通过更早的错误反馈加快了平台其他方面的开发。高质量的包存储库对于新用户的留存也非常重要。

在本文中，我们介绍了我们关于分析 OCaml 程序内存使用情况的当前工作。我们的技术允许观察跟踪类型、分配点和块的可达路径，而无需运行时成本，除了保存观察结果。

OCamlPro成立一周年后，Fabrice Le Fessant在OCaml研讨会上简要总结了这一年中所开展的工作。速查表、opam包管理器等等，都是OCaml发行版和整个社区长期贡献的开始。

这是一个双重主题的演讲，涵盖了对OCaml程序内存行为的研究以及当时OCamlPro正在开发的内存分析工具。这些工作旨在减少内存占用、查明并修复内存泄漏，以及减少运行时内存管理所花费的时间。

在opam包管理器开发启动六个月后，Frederick Tuong、Fabrice Le Fessant和Thomas Gazagnaire首次展示了日后成为OCaml发行版官方包管理器的成果。这份简短的资料涵盖了当时仓库的现状以及平台未来的展望，它承载着OCaml发展史上的重要篇章。

为什么你的下一门编程语言应该选择函数式语言。

使用Camlp4进行元编程教程

在这个演讲中，我们将首先描述XenServer和XenAPI的架构，并讨论使用基于Objective Caml的解决方案所面临的挑战。这些挑战涵盖了与Xen和Linux内核交互的底层问题，以及诸如分布式故障规划等高级算法问题。此外，我们还将讨论在商业环境中使用OCaml带来的挑战，例如支持产品升级、增强可支持性以及扩展开发团队。

本章节深入探讨了核心ML类型系统的抽象，重点介绍了类型推断。类型推断算法被描述为约束生成器（生成类型方程组）和约束求解器（表示为一组重写规则）的组合。

本文解释了为什么即使被`let`绑定的表达式不是值，在`let`绑定处泛化某些类型变量也是安全的。这种Wright经典“值限制”的放松版本是在OCaml 3.07中引入的。

本文提供了更多关于多态变体背后技术机制的细节，重点关注了对深度模式匹配结构进行类型检查的规则。

本说明描述了OCaml 3.07中引入的实验性递归模块。

本文解释了多态变体背后的大部分类型检查机制。其核心是使用所谓的局部约束扩展核心ML的类型规则。

本文提供了OCaml标记函数参数和可选函数参数的动态语义、静态语义和编译方案。

关于Caml Light和OCaml运行时系统中垃圾回收器的一切。

这篇易于理解的论文描述了OCaml模块系统的一个简化实现，强调了模块系统在很大程度上独立于底层核心语言的事实。这是一个学习如何使用模块以及如何对其进行类型检查的良好教程。

这篇简短的论文解释了如何使用多态变体设计一个模块化、可扩展的解释器。

本文提出了一种将一等多态值重新引入ML，同时保留其类型推断机制的方案。这项技术是OCaml多态方法的基础。

本文为OCaml的面向对象层提供了理论基础，包括动态语义和静态语义。

本文简要解释了多态变体的用途及其编译方式。

本文调查并比较了几种数据表示策略，包括OCaml原生代码编译器中使用的一种。

这项工作通过引入所谓的应用函子扩展了上述论文，即当应用于可证明相等的实参时产生兼容抽象类型的函子。应用函子也是OCaml的一个特性。

关于Caml Light和OCaml运行时系统中垃圾回收器的一切。

本文描述了核心ML的语义和类型系统，并使用一种简单的语法技术来证明类型正确的程序不会出错。

本文提出了Standard ML模块系统的一个变体，该变体引入了抽象类型和显式类型之间的严格区分。后者是其定义明确作为模块接口一部分出现的类型。该提案旨在保留Standard ML模块系统的大部分表达能力，同时为分离编译提供更好的支持。这项工作为OCaml的模块系统奠定了正式基础。

本文描述了Caml Light和OCaml运行时系统中垃圾回收器的并发版本。

已被“多处理器系统的可移植、不显眼的垃圾回收”取代

本报告包含 ZINC 编译器的摘要，该编译器后来演变为 Caml Light，再演变为 OCaml。本报告的很大一部分已经过时，但它仍然作为 Caml Light 中使用的抽象机的摘要（以及在 OCaml 中经过进一步简化和速度改进）具有价值。