A Core Calculus for Static Latency Tracking with Placement Types
开发高效的地理分布式应用程序是一项挑战，因为程序员可以很容易地引入需要高延迟通信的计算。我们提出了一种语言设计，使延迟明确和提取类型级别的界限计算的运行时延迟。我们提出了我们的初始步骤与核心演算，使提取可证明正确的延迟界限和概述未来的工作。
2020-07-30 cs.LO cs.PL cs.SE
DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
TU Darmstadt（达姆施塔特工业大学）；National Research Center for Applied Cybersecurity ATHENE（国家应用网络安全研究中心 ATHENE）
本文提出DeCo核心演算，通过静态增量泛化用户自定义数据类型上的领域特定操作，实现更细粒度的增量计算，并证明其正确性。
2026-02-24 cs.PL
Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions
我们的目标是推理Erlang程序的行为保持转换的正确性。行为保留的特点是语义等价。基于我们现有的形式语义的核心Erlang，我们调查合适的等价关系的潜在定义。特别是，我们适应了一些现有的表达等价的方法，一个简单的功能程序设计语言，进行顺序核心Erlang的主要特点，然后我们检查的等价关系的属性，并正式建立它们之间的连接。本文的结果，包括所有定理及其证明，已使用Coq证明助手进行了机器检查。
2022-08-30 cs.PL
The LLMbda Calculus: AI Agents, Conversations, and Information Flow
University of Nottingham, UK（诺丁汉大学）；University of Edinburgh, UK（爱丁堡大学）；Chalmers University of Technology（查尔姆斯理工大学）；The University of Gothenburg, Sweden（哥德堡大学）
本文提出了一种无类型的lambda计算模型，用于形式化描述和验证人工智能代理中对话和信息流的安全性。
2026-07-13 cs.AI cs.CR cs.PL
The Essence of JavaScript
我们将JavaScript简化为一个以小步操作语义为结构的核心演算。我们提出了几个特殊的语言，并表明我们的演算模型。我们阐述了脱糖过程，把JavaScript程序的核心。我们使用真实世界的测试套件来证明对JavaScript的忠诚。最后，我们通过定义一个安全属性来说明实用性，将其实现为核心上的类型系统，并将其扩展到完整的语言。
2015-10-04 cs.PL
A Dependent Dependency Calculus (Extended Version)
二十多年前，Abadi等人建立了依赖核心演算（DCC）作为分析类型化程序设计语言中依赖关系的通用框架。从那时起，依赖性分析已经显示出对语言设计的许多实际好处：它的结果可以帮助用户和编译器强制执行安全约束，消除死代码，以及其他应用。在这项工作中，我们提出了一个依赖依赖演算（DDC），它扩展了这个一般的想法，设置依赖类型的语言。我们使用这种演算来跟踪运行时和编译时的无关性，从而实现更快的类型检查和程序执行。
2022-02-02 cs.PL
A Core Calculus for Type-safe Product Lines of C Programs
University of Turin（都灵大学）；Toho University（东邦大学）；National Institute of Informatics（国立情报学研究所）
本文提出轻量级C核心演算及着色LC，设计类型系统确保C预处理器生成程序的类型安全性，适用于教学与研究。
2026-03-04 cs.PL cs.SE
Strong Normalization for the Calculus of Constructions
构造演算（CC）是依赖类型编程和高阶构造性逻辑的核心理论。CC最初是在Coquand 1985年的论文中提出的，它激发了程序设计语言和类型论25年的研究。今天，CC的扩展构成了Coq和Agda等语言的基础。本综述回顾了CC强规范化属性的三个证明（良好类型的表达式不存在无限约简序列）。它突出了证明结构的相似性，同时显示了它们的差异是如何被作者的不同目标所激发的。
2022-10-07 cs.PL
A Functional Programming Language with Versions
虽然现代软件开发大量使用版本化包，但程序设计语言很少在其语义中支持版本的概念，这使得软件更新更加庞大和不安全。本文提出了一种本质上支持版本的程序设计语言。其主要目标是设计核心语言功能，以支持在一个程序中的多个版本，并建立一个适当的概念，类型安全与这些功能。所提出的核心演算称为Lambda VL，具有版本化的值，每个值在不同版本下包含不同的值。我们的类型系统的建设作为一个扩展的coeffect演算的版本映射到计算资源。类型系统保证程序存在有效的版本组合。演算使程序设计语言能够在程序中使用包的多个版本。它将作为设计高级语言功能（如模块系统和语义版本）的基础。
2021-07-15 cs.PL
Extended Report: The Implicit Calculus
泛型编程（GP）是程序设计语言中一个日益重要的趋势。众所周知的GP机制，如类型类和C++0x概念提案，通常结合了两个特性：1）特殊类型的接口; 2）这些接口实现的隐式实例化。Scala隐式实例化是一种GP语言机制，受类型类的启发，打破了将隐式实例化与特殊类型的接口耦合的传统。相反，隐式实例化只提供隐式实例化，它被一般化为适用于任何类型。事实证明，这对于解决其他GP机制中出现的许多限制非常强大和有用。本文将隐式语言的核心思想形式化地综合到一个最小的、通用的核心演算中，称为隐式演算，并展示了如何在此基础上构建支持隐式实例化的源语言。隐式演算的一个新颖之处在于它支持部分解析和高阶规则（这一特性以前曾被提出，但从未被形式化或实现）。最终，隐式演算提供了一个形式化的隐式演算模型，语言设计者可以使用它来研究和通知在他们自己的语言中实现类似的机制。
2012-03-20 cs.PL
Elegant elaboration with function invocation
我们提出了一个优雅的设计的核心语言在依赖类型的λ演算与$δ$减少和细化算法。
2021-07-05 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
Explicit Effect Subtyping
随着代数效果和处理程序的普及，对其有效执行的需求也在增加。Eff是一种类似ML的语言，具有对处理程序的本机支持，它具有一个基于子类型的效果系统，可以在该系统上构建一个效果感知优化编译器。不幸的是，根据我们的经验，为Eff实现优化非常容易出错，因为它的核心语言是隐式类型的，这使得代码转换非常脆弱。为了弥补这一点，我们提出了一个显式类型的多态核心演算代数效果处理程序与子类型为基础的类型和效果系统。它具体化了在显式类型转换中的子类型化，并使用见证子类型化证明的子类型化，从而快速暴露程序转换中的类型化错误。我们的面向类型的细化带有一个基于约束的推理算法，该算法将隐式类型的Eff-like语言转换为我们的演算。此外，所有的子和效应信息都可以直接擦除，这表明子没有计算内容。此外，我们提出了一个一元的翻译从我们的演算到一个纯语言没有代数的影响或处理程序，使用效果的信息，只有在必要时才引入一元结构。
2020-05-28 cs.PL
Typed Closure Conversion for the Calculus of Constructions
依赖类型语言（如Coq）用于指定和验证源程序的完整功能正确性。类型保持编译可用于通过编译到生成的目标语言程序中来保持这些规范和正确性证明。不幸的是，依赖类型的类型保持编译是困难的。本质上，问题在于依赖类型系统是围绕高级组合抽象来设计的，以决定类型检查，但编译会干扰类型系统规则来推理运行时术语。我们开发了一个类型保持闭包转换的翻译从构造演算（CC）与强依赖对（$Σ$类型）-一个子集的核心语言Coq-到一个类型安全的，依赖类型的编译器中间语言命名为CC-CC。在这项工作中的核心挑战是如何翻译的源类型系统的规则推理功能到目标类型系统的规则推理闭包。为了证明这些规则的合理性，我们通过在CC中给出一个模型来证明CC-CC的可靠性。除了类型保持，我们证明了分离编译的正确性。
2018-08-12 cs.PL
The Mob core language and abstract machine (rev 0.2)
目前大多数移动Agent系统都是基于程序设计语言的，由于缺乏足够的形式化理论，其语义很难被证明是正确的。近年来，并发系统理论的发展，即进程演算的发展，首次允许了移动Agent系统的建模，然而直接基于进程演算的语言是非常低级的，希望在保持基本演算语义的同时，为程序员提供更高层次的抽象。在这份技术报告中，我们提出的语法和语义的脚本语言编程移动代理称为暴民。我们描述了语言的语法和语义。Mob是面向服务的，这意味着代理既充当服务器又充当服务的客户端，并且这种耦合在运行时动态完成。该语言是在一个进程演算之上实现的，它允许我们通过将其语义编码到底层演算中来证明框架是合理的。这提供了一种语言安全性，而其他使用ah-doc方法开发的移动代理语言则无法提供这种安全性。
2008-10-24 cs.DC cs.PL
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
Imperial College London（帝国理工学院）
本文提出一个支持高阶有副作用操作处理器的核心演算，通过无律原始单子与判断性单子律相结合的设计，证明了无递归片段的闭项典范性和参数性。
2025-11-07 cs.PL
On reduction and normalization in the computational core
我们研究的减少，在一个计算演算来自莫吉的计算之一，我们称之为计算的核心。归约关系由定向三个一元定律得到的规则组成。这些法则，特别是结合性和恒等式，在运算分析中引入了复杂性。我们研究了返回值与具有范式的中心概念，并解决了规范化策略的问题。我们的分析依赖于因式分解的结果。
2022-11-29 cs.LO cs.PL
Petr4: Formal Foundations for P4 Data Planes
P4是一种用于编程和指定数据包处理系统的特定领域语言。它基于一个优雅的设计，具有高级抽象，如解析器和匹配操作管道，可以编译为软件或硬件中的有效实现。不幸的是，像许多工业语言一样，P4的发展没有正式的基础。P4语言规范是一个160页的文档，混合了非正式的散文、图形图表和伪代码。P4参考实现是一个复杂的系统，运行超过40KLoC的C++代码。显然，这两种人工制品都不适合形式推理。本文提出了一个新的框架，称为Petr 4，把P4的坚实基础。Petr 4由一个干净的定义解释器和一个演算组成，该演算对P4的核心片段的语义进行建模。在整个规范中，程序行为的某些方面留给目标。我们的解释器是在一个目标接口上参数化的，该接口将规范中所有特定于目标的行为收集在一个接口中。该规范对某些程序结构的嵌套进行了特别的限制，以简化编译并避免程序不终止的可能性。我们通过对核心演算的类型系统进行分层，而不是强加不自然的语法限制，来捕捉核心演算的后一个意图，并且我们证明了核心演算中的所有程序都可以终止。我们已经通过P4参考实现中的750多个测试对解释器进行了验证，并通过针对不同目标的测试来练习我们的目标接口。我们在分层型系统上用归纳法建立了核心演算的终止性。在开发Petr 4时，我们报告了语言规范和参考实现中的数十个错误，其中许多已经修复。
2020-11-11 cs.NI cs.PL
Opportunistically Parallel Lambda Calculus
University of Pennsylvania（宾夕法尼亚大学）；University of California, Los Angeles（加州大学洛杉矶分校）
Opal通过机会性并行λ演算提升脚本语言的执行效率，显著减少外部调用的等待时间，性能优于Python和Rust。
2026-02-05 cs.PL
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
并发程序设计语言的比较和并发环境下程序转换的正确性是本文研究的重点。作为标准，我们使用的上下文语义适应并发，在那里可能-以及应该-收敛观察。本文研究了并发Haskell（CH）核心语言与同步π演算的关系。上下文语义一方面对操作语义的细节给予宽容，另一方面对翻译后过程之间的相互作用提出了强烈的要求。我们的结果是，CH包含同步π演算。我们的主要任务是通过CH的并发原语（MVars）来发现和证明π演算通道编码的正确性。它们的行为类似于（阻塞）1位缓冲区，对共享内存进行建模。第一个开发的翻译使用一个额外的私人MVar的每一个通信。我们还自动生成和检查潜在的正确的翻译，重用MVar，其中一个MVar包含的消息和两个额外的MVar同步用于模拟一个通道的同步通信的pi演算。我们的自动实验结果导致推测，一个额外的MVar是不够的。
2020-08-31 cs.LO cs.PL
Space Improvements and Equivalences in a Functional Core Language
我们探讨空间的改进LRP，一个多态类型的呼叫需要功能的核心语言。一个宽松的空间措施是选择在评估过程中的最大尺寸使用。它通过抽象机器从实现的细节中抽象出来，但它考虑了垃圾回收，因此可以被看作是空间使用的一个现实近似。其结果是：一个上下文引理的空间改进的翻译和空间等价，所有的，但一个减少规则的演算是空间的改进，并为例外，我们显示的空间增加的界限。几个进一步的程序转换被证明是空间改进或空间等价，特别是翻译成机器表达式是一个空间等价。我们还将某些空间恶化的变换归类为空间泄漏或空间安全。这些结果在预测按需调用函数式语言中优化转换的运行时空间行为的变化方面向前迈进了一步。
2018-02-19 cs.PL
A Formal Model for Direct-style Asynchronous Observables
像F#、C#和最近的Scala这样的语言提供了“异步”编程模型，旨在通过避免基于回调的编程模型中固有的控制反转来使异步编程更容易。本文提出了一种新的方法来集成异步模型与可观察流的反应式扩展模型。响应式扩展在.NET平台上最为知名，其编程模型的广泛使用的实现也存在于Java、Ruby和其他语言中。本文贡献了一个形式化的统一的“反应异步”模型的背景下，基于对象的核心演算。我们的正式模型捕捉到的异步可观的协议使用堆演化属性的本质。我们证明了一个主题约简定理，该定理意味着约简保持堆的演化性质。因此，对于良好类型的程序，我们的演算确保协议的异步可观的。
2015-11-02 cs.PL
LambdaDL: Syntax and Semantics (Preliminary Report)
语义数据推动了许多不同的应用程序，但仍然缺乏适当的集成到程序设计语言中。非类型化访问容易出错，而映射方法不能完全捕获语义数据的概念化。在本文中，我们提出了$λ_{DL}$，一个$λ$演算与修改的类型系统，提供类型安全的集成语义数据。这是通过将描述逻辑集成到用于类型化和数据访问的$λ$演算中来实现的。它围绕着几个关键的设计原则。其中包括（1）使用语义概念化作为类型，（2）这些类型的子类型推断，以及（3）通过确保查询的可满足性以及在$λ_{DL}$中精确地键入查询结果来对数据进行类型检查的查询访问。本文激励使用修改的类型系统的语义数据，它提供了理论基础的描述逻辑的集成，以及$λ_{DL}$的核心形式化规范，包括类型安全的证明。
2016-10-22 cs.PL
Package Managers à la Carte: A Formal Model of Dependency Resolution
University of Cambridge（剑桥大学）；Jane Street（简街）；Tarides
本文提出Package Calculus，通过形式化缩减展示其能统一包管理器的核心语义，为跨生态系统工具提供理论基础。
2026-07-20 cs.PL cs.SE
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
我们开发了一个线性逻辑框架内的混合系统，并使用它来推理的类型系统的量子λ演算。特别是，我们认为一个实用的版本的演算称为原Quipper，其中包含的核心Quipper。Quipper是一种正在积极开发的新量子程序设计语言，最近在量子计算社区中获得了很大的普及。Hybrid是一个系统，旨在支持使用高阶抽象语法（HOAS）来表示和推理Coq证明助手中实现的正式系统。在这项工作中，我们扩展了系统的线性规格说明逻辑（SL），以理由Quipper的线性型系统。为此，我们形式化的原型Quipper的语义编码的SL中的类型和评价规则，并证明类型的可靠性。
2018-12-10 cs.LO cs.PL
Compositional theories for host-core languages
本文扩展了Benton的线性-非线性类型理论，提出宿主-核心类型理论及类型化演算HC，通过充实范畴提供指称模型，并利用内部语言概念建立语法与语义的强对应关系，为多语言编程提供理论支持。
2024-06-26 cs.LO cs.PL
h: A Plank for Higher-order Attribute Contraction Schemes
我们提出并形式化h，一个核心（或“木板”）演算，可以作为基础的几个编译器规约语言，特别是CRSX（组合约简系统与扩展），HACS（高阶属性收缩方案），和transScript。我们讨论了h类型和形成规则如何引入必要的限制，以确保重写是定义良好的，即使在h的强大的扩展操作自由变量和环境作为第一类元素（包括在模式匹配）的存在。
2017-11-09 cs.LO cs.PL
On Compensation Primitives as Adaptable Processes
我们比较机制的补偿处理和动态更新演算的并发。这些机制在可靠通信系统的规范中越来越重要。补偿和更新在直观上是相似的：两者都指定并发系统的行为在运行时如何响应异常事件而改变。然而，具有补偿和更新的结石在技术上是完全不同的。我们调查这些结石的相对表现力：我们开发的核心过程语言的编码与补偿到一个适应性强的过程在以前的工作中开发的演算。我们的编码揭示了补偿处理及其关键结构的（复杂）语义。它们还可以将现有的验证和推理技术转移到具有补偿处理的核心语言中。
2015-08-27 cs.LO cs.PL
