Indexed realizability for bounded-time programming with references and type fixpoints
隐式复杂性领域最近产生了几种有界复杂性程序设计语言。这种语言允许精确地实现属于某个复杂类的函数。我们在这里提出了一个实现语义的高阶函数语言的基础上的线性逻辑称为LAL的复杂性类PTIME的特点的片段。这种语言的特点是递归类型和高阶存储。我们的可实现性是基于双正交性，步进索引，而且是定量的。这最后一个功能，使我们不仅可以得到一个语义证明的终止，但也给类型化程序终止所需的计算步骤的数量上的界限。
2012-06-21 cs.LO cs.PL
Towards Patterns for Heaps and Imperative Lambdas
在函数式程序设计中，无点关系演算在程序构造的一般理论中已经取得了丰硕的成果，但对于特定的应用程序，逐点表达式可以更方便和更容易理解。在命令式编程中，精化演算已经被绑定到状态变量的逐点表达式，除了无处不在但不可见的堆。为了将点态与无点态结合起来，de Moor和Gibbons扩展了λ演算，并使用关系解释了非单射模式匹配。本文给出了该语言的一种语义，使用偏序之间的“理想关系”，以及使用谓词Transformers的第二种语义。第二种语义的动机是它与分离代数的潜在用途，用于作用于堆的程序中的模式匹配。在这些模型中，包括松弛贝塔和埃塔法律证明，并提出了一些开放的问题。
2015-10-19 cs.PL
The lambda mechanism in lambda calculus and in other calculi
兰丁的λ演算形式与丘奇的比较表明，独立于λ演算，存在一种机制，用于将参数由变量索引的函数转换为参数由数字索引的通常类型的函数。我们称之为“lambda机制”，并展示了如何在其他演算中使用它。在一阶谓词逻辑中，它可以用来定义新的函数和新的谓词。在纯命令式程序设计语言中，它可以用来提供类似于Algol的过程设施。
2015-05-28 cs.PL
The semantic marriage of monads and effects
Wadler和Thiemann通过一个语法对应和可靠性结果，将类型和效果系统与一元语义统一到操作语义上。他们推测，一个一般的，“连贯的”指称语义可以给出统一的效果系统与单子式的语义。我们提供了这样一个语义的基础上的索引单子，我们介绍的新结构。我们重新定义的语义Moggi的计算计算的Alzida演算（强）索引单子，它给出了一个一对一的对应关系之间的索引的表示和传统的效果系统的效果注释。双重地，这种方法产生索引的comonads，它为上下文的效果概念（称为coeffects）提供了统一的语义和效果系统，我们之前已经描述过。
2014-01-21 cs.PL
Relating Functional and Imperative Session Types
本文通过构造保持类型与语义的翻译，证明函数式会话类型包含命令式会话类型，并指出后者表达力不足主要源于其类型系统限制。
2022-09-14 cs.PL
A Type System Theory for Higher-Order Intensional Logic Support for Variable Bindings in Hybrid Intensional-Imperative Programs in GIPSY
我们描述了一个类型系统的平台称为一般内涵编程系统（GIPSY），旨在支持内涵程序设计语言的内涵逻辑和他们的强制性对应部分的内涵执行模型。在GIPSY中，类型系统在其编译器和运行时环境中粘合了内涵和命令式语言之间的静态和动态类型，以支持以内涵程序设计语言Lucid的各种方言编写的表达式的内涵求值。内涵使表达式明确考虑到多维的评估上下文，上下文是一个一流的值，服务于许多需要上下文概念来进行的应用程序。我们描述和讨论这样一个类型系统的属性和相关的类型论，以及GIPSY类型系统的语义，设计和实现的特殊性。
2009-06-22 cs.LO cs.PL
ImNet: An Imperative Network Programming Language
最新的网络架构之一是软件定义网络（SDN），其使用控制器设备来控制网络上的交换机集合。控制过程包括在交换机的流表上安装或卸载分组处理规则。本文提出了一种高级命令式网络程序设计语言，称为ImNet，以方便编写高效，但简单，由控制器执行的程序来管理交换机。ImNet结构简单，具有表达性，组合性和命令性。本文还介绍了一个操作语义的ImNet。文中还给出了在ImNet中构造的程序（及其操作语义）的详细实例。
2014-02-23 cs.NI cs.PL
The Functional Machine Calculus III: Control
University of Bath（巴斯大学）
本文提出了一种扩展的函数机器演算，支持分支和循环控制流，统一了函数式和命令式编程范式。
2026-02-27 cs.LO cs.PL
A Semantics for Probabilistic Control-Flow Graphs
本文提出了一种新的操作语义的概率控制流图（pCFG）的概率命令式程序与随机分配和“观察”（或条件）语句。当控制从pCFG中的一个节点移动到另一个节点时，语义转换概率分布（在商店上）。我们将此语义的标准，预期转换，指称语义的结构化概率命令式程序，结构化程序翻译成（非结构化）pCFGs，并证明充分的翻译。这表明操作语义可以在不丢失信息的情况下使用，并且忠实于“预期”语义，因此可以用于推理，例如，转换的正确性（正如我们在配套文章中所做的那样）。
2017-11-07 cs.PL
Logical Step-Indexed Logical Relations
Appel和McAllester的“step-indexed”逻辑关系已被证明是一种简单而有效的技术，用于推理具有语义上有趣的类型（如通用递归类型和通用引用类型）的语言中的程序。然而，使用步骤索引模型的证明通常涉及繁琐，容易出错和证明模糊的步骤索引算法，因此重要的是要开发干净，高级，等式证明原则，避免提及步骤索引。在本文中，我们展示了如何以一种抽象而优雅的方式推理二进制步进索引逻辑关系。具体来说，我们定义了一个逻辑LSLR，它的灵感来自于Plotkin和Abadi的参数化逻辑，但也支持递归定义的关系，通过模态“后来”的运营商从Appel，Melliès，Richards，和Quillon的“非常模态模型”的文件。我们在LSLR编码的逻辑关系的推理相关的程序调用的值系统F扩展一般递归类型。利用这种逻辑关系，我们得到了一组有用的规则，我们可以证明上下文等价和近似结果，而不计步骤。
2011-06-06 cs.LO cs.PL
Imperative Quantum Programming with Ownership and Borrowing in Guppy
Quantinuum
本文提出一种结合线性类型与指令式语义的量子类型系统，并在 Guppy 语言中实现，以在指令式量子编程中保持安全保证。
2025-10-15 cs.PL cs.SE quant-ph
Reactive Imperative Programming with Dataflow Constraints
数据流语言为动态应用程序中指定对象之间的约束提供了自然支持，其中程序需要有效地对环境的变化做出反应。研究人员长期以来一直在研究如何通过将它们嵌入到过程语言中来利用Challow-constraints。然而，以前的混合命令式/并行系统需要语法扩展或专门的数据类型库来将命令式程序绑定到并行求解器。在本文中，我们提出了一种新的方法，顺利地结合了这两种范式，而不会给程序员带来不必要的负担。在我们的框架中，程序员可以定义主机命令式语言的普通命令，这些命令强制执行存储在“反应式”内存位置中的对象之间的约束。反应对象可以是宿主语言中的任何合法类型，包括基本数据类型、指针、数组和结构。约束在每次输入内存位置改变时自动重新执行，让程序表现得像电子表格，其中某些变量的值取决于其他变量的值。通过改变宿主语言的基本操作的语义来读取和修改对象，从而透明地处理约束求解机制。我们提供了一个正式的语义和描述我们的技术到C/C++的一个具体实施例，展示了如何有效地实现它在传统的平台上使用现成的编译器。我们讨论了相关的应用反应的情况下，包括增量计算，观察者设计模式，和数据结构修复。我们的实现的性能相比，特设问题特定的变化传播算法和以语言为中心的方法，如自调整计算和主体/观察者通信机制，表明所提出的方法是有效的，在实践中。
2011-04-12 cs.PL
Sequence Types and Infinitary Semantics
我们引入了一个新的表示非幂等交集类型，使用\textbf{sequences}（家庭索引的自然数），而不是列表或多集。这允许将\textbf{intersection type}理论扩展到无限$λ$ -演算。因此，我们的特点是遗传头部正常化，这给出了一个积极的答案，被称为\textbf{Klop's Problem}的问题。在我们的方法中，我们使用\textbf{non-idempotent intersection}检索一些著名的结果无穷项。
2021-12-15 cs.LO cs.PL
A Model of Cooperative Threads
我们开发了一个模型的并发命令式编程线程。我们专注于一个小的命令式语言与合作的线程，执行无中断，直到他们终止或显式地产生控制。我们定义并研究了这种语言的基于跟踪的指称语义，这种语义是完全抽象的，但数学上是初等的。我们还给出了一个方程理论的计算效果，基础的语言，包括线程产卵。然后，我们分析线程的自由代数单子这个理论。
2010-10-20 cs.PL
ImpNet: Programming Software-Defied Networks Using Imperative Techniques
软件和硬件组件是现代网络的基本组成部分。但软件组件是典型的封闭式和面向功能的。因此，很难修改这些组件。这严重影响了网络创新。此外，这导致网络策略具有用户不友好的复杂接口，并因此导致网络的物理交换机上的巨大且复杂的流表。这在许多情况下会大大降低网络性能。软件定义网络（SDN）是一种现代网络架构，可以克服上述问题。SDN的思想是向网络添加控制器设备，该控制器设备管理网络上的所有其他设备，包括网络的物理交换机。管理过程的主要任务之一是交换机学习;通过对网络的物理交换机进行编程来实现，通过向交换机（更具体地说，向交换机的流表）添加或从交换机（更具体地说，从交换机的流表）移除用于分组处理的规则。本文提出了一种高级命令式网络程序设计语言--ImpNet。ImpNet允许编写高效，但简单，功能强大的程序在控制器上运行，以控制所有其他网络设备，包括交换机。ImpNet是组合的，结构简单，富有表现力，更重要的是命令式的。介绍了ImpNet的语法以及ImpNet合同的两种操作语义。所提出的语义是静态和动态类型。两个现代应用程序编程使用ImpNet的文件中显示。文中还给出了应用程序的语义。
2014-07-08 cs.NI cs.PL
Recovering Purity with Comonads and Capabilities
在本文中，我们采用了一种普遍有效的（ML风格的）类型λ演算，并展示了如何扩展它以允许捕获具有类型的纯表达式。我们的关键观察是，正如纯简单类型的λ演算可以扩展到支持一元类型规则的效果，不纯类型的λ演算可以扩展到支持一元类型规则的纯度。我们通过一个简单的指称模型来建立我们的类型系统的正确性，我们称之为能力空间模型。我们的模型形式化的直觉常见的系统程序员，执行效果的能力应该通过访问权限或能力进行控制，一个程序是能力安全的，如果它没有执行效果，它没有一个运行时的能力。然后，我们确定的公理范畴结构的能力空间模型验证，并使用这些公理给我们的comonadic类型系统的范畴语义。然后，我们给出了一个等式理论（替代和调用的值$β$和$η$法律）的命令λ演算，并显示其可靠性相对于此语义。最后，我们给出了一个翻译的纯简单类型的λ演算到我们的共同命令演算，并表明，任何两个条款是$βη$ -平等的STLC是平等的共同命令演算的方程理论，建立纯程序可以映射到我们的命令演算在一个方程保持的方式。
2020-11-10 cs.LO cs.PL
The While language
本文给出了一种简单的命令式程序设计语言的形式化。目标是研究和开发“动手”的程序设计语言的形式规范，即它的语法，操作语义和类型系统。为了获得该语言的可执行版本，我们在Racket中实现了它的操作语义和类型系统。
2016-04-12 cs.PL
Abstracting an operational semantics to finite automata
命令式程序的小步操作语义的描述与有限自动机的语义有明显的相似性，因此定义一个从语义到自动机的抽象映射并证明一个模拟性质似乎是容易的。本文的目的是确定原因简单的证明打破，其中工件的语义，导致口吃的模拟步骤。然后，我们提出了一个语义的基础上的拉链数据结构，与直接解释的评价导航的语法树。然后通过等价类构造来定义抽象函数。
2014-09-27 cs.PL
Denotational semantics of general store and polymorphism
本文首次提出结合卫递归与非直谓多态性的多态依赖类型理论指称语义，支持一般高阶引用和递归类型，并通过“逻辑关系即类型”的模态构造实现对有状态抽象数据类型的关系推理。
2023-04-12 cs.LO cs.PL
Deriving Abstract Interpreters from Skeletal Semantics
本文提出一种基于骨架语义及其语义元语言抽象解释的方法，从编程语言形式化语义派生可执行抽象解释器，并通过小型命令式语言的值分析验证了其通用性与正确性。
2023-09-13 cs.PL
A Linear First-Order Functional Intermediate Language for Verified Compilers
我们提出了线性一阶中间语言IL验证编译器。IL是一种函数式语言，可以调用非确定性环境。我们给IL条款的第二个，命令式语义解释，并获得一个寄存器转移语言。对于命令式解释，我们建立了活变量的概念。基于活变量，我们制定了一个可判定的属性称为一致性，确保功能和命令的解释一个术语相吻合。我们制定了一个寄存器分配算法的IL，并证明其正确性。该算法将一个函数式IL程序转换为一个等价的命令式IL程序。正确性来自于这样一个事实，即算法在一致地重命名局部变量后达到了一个连贯的程序。我们证明了初始程序中的最大活变量数限制了最终相干程序中不同变量的数量。整个开发都在Coq中正式化。
2015-06-04 cs.PL
Syntax and Semantics of Linear Dependent Types
本文提出了一种类型论，它把（直觉）线性类型与类型依赖相结合，从而适当地推广了直觉依赖类型论和完全线性逻辑。语法和完整的范畴语义的发展，后者在（严格）索引对称monoidal范畴的理解。以模块化方式处理各种可选类型的成形器。特别是，我们将看到，历史上备受争议的乘法量词和身份类型自然地产生于范畴考虑。这些新的乘法连接词的进一步特点是由几个身份有关的依赖类型论和线性逻辑通常的连接词。最后，详细研究了一类重要的模型，即由值在某个对称monoidal范畴内的族给出的模型。
2015-01-16 cs.LO cs.PL math.CT
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
可靠的演绎程序验证技术应该被证明是相对于程序设计语言的语义合理的。对于每一种不同的语言，构造一个单独的可靠性证明往往是一项艰巨的任务。在独立于语言的程序验证中，讨论了计算机程序的共同方面，以使所有语言都能进行合理的推理。在这项工作中，我们提出了一个解决方案，合理的推理迭代和递归的基础上的大步骤操作语义的任何程序设计语言。我们给出了我们的推理技术的合理性和相对完整性的归纳证明。我们说明了在简化的程序设计语言的命令式和功能的范例，具有不同的功能的技术。我们还在Coq证明助手中机制化所有正式结果。
2021-08-04 cs.PL
Persistent Iterators with Value Semantics
National University of Singapore（新加坡国立大学）
本文提出持久迭代器，结合了命令式语言的迭代风格与持久数据结构的语义，通过快照容器版本确保安全，实现真正的值语义，提升表达力并消除迭代器失效问题。
2026-04-15 cs.PL
Explicit and Controllable Assignment Semantics
尽管有大量强大的软件可以发现错误，识别性能瓶颈或简单地提高代码的整体质量，但程序设计语言仍然是开发人员的第一个也是最重要的工具。因此，适当的抽象、明确的语法和直观的语义对于简洁有效地传达意图至关重要。计算能力的持续增长使现代编译器和运行时系统能够处理曾经被认为不切实际的功能，如类型推断和反射，使代码更容易编写，更容易阅读。不幸的是，在大多数程序设计语言中，底层内存模型的残余仍然存在，导致了混乱的赋值语义。本文介绍了Anzen，一种程序设计语言，旨在使任务更容易理解和操作。该语言提供了三个赋值运算符，具有明确的语义，可以重现所有常见的命令式赋值策略。它伴随着一个基于类型功能的类型系统，以强制唯一性和不变性。我们提出了Anzen的功能非正式和形式化的手段，一个最小的演算。
2019-07-25 cs.PL
Interacting via the Heap in the Presence of Recursion
几乎所有现代命令式程序设计语言都包含动态操作堆的操作，例如通过分配和释放对象，以及通过更新引用字段。在递归过程和局部变量的存在下，程序与堆的交互可能变得相当复杂，因为可以使用局部变量在调用堆栈上分配无限数量的对象，或者匿名地使用引用字段在堆上分配对象。因此，一般来说，静态分析是不可判定的。在本文中，我们研究了验证的递归程序与无界分配的对象，在一个简单的命令式语言堆操作。我们提出了一种改进的语义，这种语言，使用的抽象是精确的。对于任何具有有界可见堆的程序，这意味着在任何执行点从变量可到达的对象数量是有界的，这种抽象是其行为的有限表示，即使在状态中可能出现无限数量的对象。因此，对于这样的程序，模型检验是可判定的。最后，我们介绍了一个规约语言的时间属性的堆，并讨论了模型检验这些属性对堆操作程序。
2012-12-17 cs.LO cs.PL
A Denotational Semantics for First-Order Logic
在Apt和Bezem [AB 99]（见CS.LO/9811017）中，我们提供了一个一阶公式的计算解释，而不是任意解释。在这里，我们补充这项工作，介绍了一个指称语义的一阶逻辑。此外，通过允许将非基础项分配给变量，我们在这个框架中引入了逻辑变量。语义学结合了许多来自命令式程序设计语言和逻辑编程的语义学领域的著名思想。在由此产生的计算视图中，合取对应于顺序组合，析取对应于“不知道”的不确定性，存在量化对应于局部变量的声明，否定对应于“否定为有限失败”规则。可靠性结果表明了语义关于真的概念的正确性。该证明在某些方面类似于SLDNF解决方案的可靠性证明。
2000-05-08 cs.AI cs.PL
Forte: A sensitivity type system for imperative Rust
Forte 是一个基于所有权机制的 Rust 敏感性类型系统，通过独占借用强更新敏感性环境，实现差分隐私程序的度量保持，并已通过 Verus 验证和 Flux 集成，在 OpenDP 机制内核上成功应用。
2026-09-25 cs.PL
Patterns for Name Analysis and Type Analysis with JastAdd
在过去的二十年里，工具已经实现了更正式地指定编译器的语义分析阶段，而不是依赖于手写代码。在本文中，我们介绍了模式和方法来翻译一种语言的类型系统的正式定义到JastAdd，这是上述工具的基础上引用属性语法的规范。这种方法将有助于语言设计者和编译器工程师更系统地使用这些工具进行语义分析。作为一个例子，我们使用了一个简单的，但完整的命令式语言，并提供了一个展望的方法可以扩展到进一步的语言结构，甚至类型推断。
2020-02-05 cs.PL
Semantic preservation for a type directed translation scheme of Featherweight Go
轻量级Go（FG）是一个最小的核心演算，包括基本的Go功能，如重载方法和接口类型。FG程序的动态行为的最直接的语义描述是基于运行时类型信息解析方法调用。一种更有效的方法是应用类型导向的翻译方案，其中接口值被包含具体方法定义的字典替换。因此，方法调用可以通过在字典中简单查找方法定义来解决。建立经由类型定向翻译方案获得的目标程序保持原始FG程序的语义是重要的任务。为了建立这个属性，我们使用了逻辑关系，这些逻辑关系是通过类型来索引的，以将源程序和目标程序联系起来。我们提供了严格的证明，并详细讨论了我们遇到的许多微妙的角落，包括由于递归接口和方法定义需要一个步骤索引。
2022-06-20 cs.PL
For Generalised Algebraic Theories, Two Sorts Are Enough
Eötvös Loránd University（罗兰大学）；LIX, CNRS, Inria, École polytechnique, Institut Polytechnique de Paris（LIX实验室，法国国家科学研究中心，Inria，巴黎综合理工学院，巴黎理工学院）
本文证明任何广义代数理论均可简化为仅含两类的理论，并通过语义方法实现商归纳-归纳类型的构造。
2026-11-11 cs.LO cs.PL math.CT
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
Denison University（丹尼森大学）；Carnegie Mellon University（卡内基梅隆大学）
本研究提出一种基于归纳定义的big-stop semantics大步语义扩展，仅添加少量规则即可捕获发散计算，且与小步迁移自反传递闭包等价，在保持易用性的同时弥补了传统大步语义的表达局限。
2025-10-22 cs.PL
An experiment with denotational semantics
本文介绍了如何按“逆序”，即从表示到语法，系统地设计一门程序设计语言。这种结构是在一个代数框架中开发的，该框架由三个多排序代数组成：表示法，抽象语法和具体语法。这些代数是以这样一种方式构造的，即从具体语法到指称存在唯一的同态，这构成了语言的指称语义。除了它的代数框架，该模型是集合论的，即指称域只是集合，而不是斯科特的自反域。该方法说明了一个虚拟语言Lingua的逐层开发：一个应用层，一个命令层（递归过程）和一个SQL层，其中Lingua被视为一个API（应用程序编程接口）的SQL引擎。后者也被赋予了指称语义。该语言配备了强大的打字机制，涵盖了基本类型（数字，布尔等），列表、数组、记录及其任意组合，以及类似SQL的类型：行、表和数据库。类型模型包括SQL完整性约束。
2019-05-04 cs.PL
A Lambda-Calculus Foundation for Universal Probabilistic Programming
我们开发的操作语义的无类型的连续分布的概率λ演算，通用概率程序设计语言，如教会，圣公会，和风险的基础。我们的第一个贡献是适应经典的操作语义的连续设置，通过创建一个测量空间的条款和定义步骤索引的近似。我们证明了这种基于分布的语义的大步和小步配方的等价性。为了更接近推理技术，我们还将术语的基于采样的语义定义为从随机样本的轨迹到值的函数。我们表明，通过整合所有的痕迹，导致的分布等于基于分布的语义。我们的第二个贡献是形式化的跟踪马尔可夫链蒙特卡罗（MCMC）的实现技术，我们的演算，并显示其正确性。一个关键的步骤是定义充分条件的分布引起的跟踪MCMC收敛到基于分布的语义。据我们所知，这是高阶函数式语言的跟踪MCMC的第一个严格正确性证明。
2017-01-23 cs.PL
SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
Oracle
提出SEMBridge框架，通过无标签最终风格统一生成可执行语义、最弱前置条件验证条件和有界检查，保持三者同步。
2026-05-29 cs.AI cs.PL
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
我们调查表示的强制性程序作为约束霍恩条款。从操作语义转换规则开始，我们着手编写解释器作为受约束的霍恩子句程序直接编码的规则。然后，我们专门一个解释器相对于一个给定的源程序，以实现编译的源语言霍恩条款（第一个二村投影的实例）。该过程是详细描述了一个解释器的一个子集的C语言，直接编码的大步骤操作语义的规则。类似的翻译基于小步语义可以进行，但我们展示了一种方法来获得一个小步表示使用线性解释器大步霍恩条款。该解释器再次专门用于实现从大步到小步风格的翻译。使用第三个解释器可以将线性小步程序转换回大步非线性程序。使用Tarjan算法计算线性规划的正则路径表达式，然后该正则表达式引导解释器计算程序路径。在所有的转换阶段，我们使用一个既定的部分评估器和利用标准的逻辑程序转换，以消除冗余的数据结构和参数的谓词和重命名的谓词，以明确其链接到原始源程序中的语句。
2020-08-07 cs.LO cs.PL cs.SC
Pyrosome: Verified Compilation for Modular Metatheory
Pyrosome 是一个 Coq 实现的模块化元理论框架，通过归纳等价保持实现可扩展的验证编译，支持特性扩展和编译器垂直组合，并展示了从 System F 到 CPS 及闭包转换的多遍编译案例。
2025-07-08 cs.PL
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
最近的许多研究都致力于在类型论中对效应进行建模。在这项工作的基础上，我们观察到，有效的类型论可以提供一个基础上建立更复杂的编程结构和程序逻辑的语义，扩展的推理原则，适用于主机有效的类型论本身。具体地说，我们的主要贡献是一个语义的并发分离逻辑（CSL）内的F* 证明助手的方式，使依赖类型，有效的F* 程序利用并发性和指定和验证使用功能齐全，可扩展的CSL。与以前的方法相比，我们直接从非确定性交织原子动作的有效语义中的计算表示中推导出CSL的部分正确性Hoare规则。展示我们的语义的灵活性，我们建立通用的，验证库，支持各种并发结构，从动态分配，可存储的自旋锁，协议索引的通道。我们的结论是，我们有效的语义提供了一个简单而富有表现力的基础上，层域特定的语言和逻辑验证，并发编程。
2021-11-30 cs.PL
