A Calculus for Language Transformations
在本文中，我们提出了一个演算表示算法的程序设计语言转换。我们给出了该演算的类型系统和操作语义，并证明了它是类型健全的。我们已经实现了我们的演算，我们证明了它的适用性与常见的例子在程序设计语言。由于我们的演算操纵推理系统，我们的工作原则上可以应用于逻辑系统。
2019-10-25 cs.PL
S-Program Calculus
本文给出了一阶谓词逻辑的一个特殊子集S-程序演算（简称S-演算）。S-演算是一种演算，由在虚拟机的抽象状态空间上定义的所谓S-公式组成。我们表明，S-公式是一个高度通用的工具，用于分析程序的语义，因为霍尔三元组的全部和部分的正确性不超过两个S-公式。此外，霍尔逻辑的所有规则都可以由S-公式和一阶谓词演算的公理/定理导出。S-演算是一种强大的机制，用于证明程序的正确性，以及使用谓词逻辑的定理构建额外的证明工具。每个证明都是基于导出一些S-公式的有效性，所以这个过程可以使用自动定理证明器（我们将在本文中使用Coq）来自动化。作为使用S-演算的一个例子，我们将证明Dijsktra算子wp的四个基本性质。Dijkstra给出的证明并没有完全形式化，我们将证明使用S-演算可以实现完全形式化。最后，我们在上述四个定理的基础上再增加一个定理，即否定律。
2010-03-03 cs.LO cs.PL
A Polymorphic RPC Calculus
RPC演算是多层程序设计语言（如Links）的简单语义基础，在Links中可以为客户端-服务器模型编写定位函数。随后，类型化RPC演算被设计成按类型捕获函数的位置信息，并驱动位置类型导向的切片编译。然而，位置的使用目前仅限于单态的，这是要克服的差距之一，将RPC演算的客户端-服务器模型的理论付诸实践。本文提出了一种多态RPC演算，允许程序员编写简洁的多层程序使用多态位置结构。然后，多态多层程序可以自动转换成程序只包含位置常数服从现有的切片编译方法。我们制定了多态RPC演算的类型系统，并证明其类型可靠性。此外，我们还设计了一个单态化翻译，并证明了翻译的类型和语义正确性。
2020-05-25 cs.PL
A Typed Slicing Compilation of the Polymorphic RPC Calculus
多态RPC演算允许程序员使用多态位置构造编写简洁的多层程序。然而，到目前为止，它缺乏执行。我们开发了一个实验性的程序设计语言的多态RPC演算的基础上。我们引入了一个多态的客户端-服务器（CS）演算与客户端和服务器部分分离。与现有的无类型CS演算相比，我们的演算不仅能够静态地解决多态位置，而且还能够动态地这样做。我们设计了一个基于类型的切片编译的多态RPC演算到这个CS演算，证明类型和语义的正确性。我们提出了一种方法，删除不必要的类型执行，但保留在运行时的位置，通过翻译的多态CS演算成一个无类型的CS演算，证明语义的正确性。
2021-07-27 cs.PL
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。
2016-09-05 cs.LO cs.PL
Continuation calculus
带有控制的程序通常使用扩展了控制算子的λ演算建模。我们不修改λ演算，而是考虑一种不同的计算模型。我们介绍连续演算，或CC，确定性的计算模型，仅使用头减少评估，并认为它是适合的建模程序与控制。它演示了如何定义程序，指定它们，并证明它们是正确的。这是通过在CC中呈现一个列表乘法程序来详细展示的，该程序在遇到零时过早返回。正确性证明包括程序的终止。在连续演算中，我们可以对按名称调用和按值调用进行建模。此外，按名称调用函数可以应用于按值调用结果，反之亦然。
2013-09-05 cs.LO cs.PL
A Core Calculus for Documents
本文针对文档与程序混合语言缺乏形式化基础的问题，提出文档演算层次模型，用于实现响应式特性并证明内容与计算边界定理，为文档语言设计提供理论依据。
2023-11-14 cs.PL
Corps: A Core Calculus of Hierarchical Choreographic Programming
本文提出层次化编排编程概念，并设计了语言Corps，通过授权逻辑中的命题即类型解释，将数据所有权建模为模态，解决了通信非线性建模与逻辑对应问题。
2024-06-03 cs.PL
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming without Space Leaks
函数式反应式编程（FRP）是一种使用信号和事件进行编程的范例，允许用户在高抽象级别上描述反应式程序。要做到这一点，FRP语言必须确保所有程序都是因果关系的，并且可以在不引入空间泄漏和时间泄漏的情况下实现。为此，某些FRP语言不提供对信号的直接存取，而只是提供对信号函数的存取。最近，模态类型已被建议作为一种替代方法，以确保在同步情况下的FRP语言的因果关系，直接存取的信号和事件的抽象。本文提出了一种新的反应式编程模式演算Simply RaTT。与以前的演算不同，Simply RaTT使用Fitch风格的方法来处理模态类型，这简化了类型系统，使程序更加简洁。呼应Krishnaswami以前的结果为不同的语言，我们设计了一个操作语义，安全地执行简单的RaTT程序没有空间泄漏。我们还确定了其他模态FRP语言中存在的时间泄漏的来源：延迟计算中不动点的展开。Simply RaTT型系统消除了这些时间泄漏。
2019-06-11 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
A Well-typed Lightweight Situation Calculus
University of California, Riverside（加州大学河滨分校）
情境演算在人工智能相关领域有着广泛的应用。这种形式主义被认为是逻辑程序设计语言的方言，主要用于动态领域建模。然而，类型系统几乎没有部署在文献中的情况演算。为了实现一个正确的和健全的有类型的程序编写的情况演算，将类型元素添加到当前的情况演算将是非常有帮助的。在本文中，我们建议增加更多的类型化机制，特别是在情况演算的三个基本元素：情况，动作和对象，然后执行严格的类型检查现有的情况演算程序，找出良好的类型和不良类型的。这样，基于我们的类型系统的类型检查可以保证情景演算程序的类型正确性和可靠性。这种轻量级的情况演算的修改版本被证明是一个强大的和良好的类型的系统。
2012-06-15 cs.AI cs.PL
A polynomial time λ-calculus with multithreading and side effects
轻逻辑的框架已被广泛研究，以控制高阶函数程序的复杂性。我们提出了一个扩展的框架，多线程程序的副作用，专注于多项式时间的情况下。在引入一个具有并行复合和区域的模态λ演算后，我们证明了对于一类良构程序，一个现实的按值调用求值策略可以在多项式时间内计算出来.结果依赖于模拟调用的值由多项式浅优先的策略，保持评估顺序的副作用。然后，我们提供了一个多项式类型系统，保证良好类型的程序不会出错。最后，我们通过一个并发迭代在归纳数据结构上产生副作用的编程例子来说明类型系统的表达能力。
2012-09-26 cs.PL
Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints
本文提出类型驱动的提示编程框架Lambda Prompt，通过依赖类型演算与概率精化表达句法和语义约束，并针对约束表达与算法支持不足提出优化规则及编译器研究方向。
2025-08-17 cs.FL cs.PL
Automatic verification of heap-manipulating programs
研究了命令式程序设计语言中堆组合推理的理论基础。本文提出了一种新的组合符号记忆的概念及其相关性质。我们利用这些正式的基础，建立一个组合算法，产生广义堆，符号堆演算，其特征在于任意循环代码段的条款。由这个演算推断出的所有状态都精确地对应于原始程序的可达状态。我们建立在这个演算和纯二阶函数程序的执行推理之间的对应关系。
2019-06-26 cs.PL
Evaluation of Logic Programs with Built-Ins and Aggregation: A Calculus for Bag Relations
我们提出了一个计划，用于翻译逻辑程序，这可能会使用聚合和算术，代数表达式表示袋关系的Herbrand宇宙的地面条款。为了评估这些关系的查询，我们开发了一个操作语义的基础上长期重写的代数表达式。这种方法可以利用算术恒等式并恢复一系列有用的策略，包括延迟工作直到它变得可能或必要的懒惰策略。
2020-10-20 cs.PL cs.SC
Formalizing Box Inference for Capture Calculus
针对捕获演算中Box符号负担重、难以集成到主流语言的问题，本文提出Box推断的形式化方案，构建半算法变体及类型层推断系统，并证明其可靠性与完备性。
2023-06-10 cs.PL
Elementary affine $lambda$-calculus with multithreading and side effects
线性逻辑提供了一个框架来控制高阶函数程序的复杂性。我们提出了一个扩展这个框架的程序与多线程和副作用的情况下，小学时间为重点。我们的主要贡献如下。首先，我们提供了一个新的组合证明终止在初等时间的功能的情况下。其次，我们开发了一个扩展的方法，以调用的值$lambda$-演算多线程和副作用。第三，我们引入了一个基本的仿射型系统，保证标准的主题约简和进步属性。最后，我们说明了规划的迭代函数的副作用所提出的形式主义。
2011-06-10 cs.PL
Tropical Mathematics and the Lambda Calculus I: Metric and Differential Analysis of Effectful Programs
本文研究 lambda 演算在热带数学框架中的解释，提出一个统一程序度量与资源分析的定量语义框架，并基于热带半环加权关系模型分析带效应程序行为，揭示了其与广义度量空间理论的抽象对应基础。
2023-11-27 cs.LO cs.PL math.LO
Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。
2015-01-15 cs.LO cs.PL
Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes
本文提出一种以目的地为核心的纯函数式线性 λ 演算，通过模态类型系统同时管理线性性与作用域，统一了现有目的地传递系统并扩展了纯函数式语言的表达能力，其类型安全性已在 Coq 中形式化验证。
2025-03-10 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
A Formal Model for Programming Wireless Sensor Networks
在本文中，我们提出了新的发展的表现力和传感器网络（CSN）的微积分理论。我们结合了一个网络层的传感器设备与本地对象模型来描述传感器设备的状态。由此产生的演算非常小，但非常有表现力。我们还提出了一个类型系统和类型不变性结果的演算。这些结果为程序设计语言和运行时环境的开发提供了基本框架。
2007-02-07 cs.DC cs.PL
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
结构编辑器允许程序员直接编辑程序的树结构。这可以带来认知方面的好处，特别是对于新手和最终用户程序员。它还简化了工具设计人员的工作，因为他们不需要处理格式错误的程序文本。本文定义了Hazelnut，一个基于小型双向类型的λ演算的结构编辑器，该演算扩展了孔和光标。Hazelnut超越了语法的良构性：它的编辑操作在静态有意义的不完整术语上操作。简单地说，这将迫使程序员以严格的“由外而内”的方式构造术语。为了避免这个问题，动作语义会自动将指定了与预期类型不一致的类型的术语放置在一个洞内。这安全地推迟了类型一致性检查，直到孔内的项完成。Hazelnut是类型化结构编辑的基本类型理论，而不是最终用户工具本身。为此，我们描述了如何榛子丰富的元理论，我们已经机械化的Agda，指导定义的扩展到微积分。我们还讨论了各种似是而非的评价策略，与孔的条款，并在这样做揭示了逐步类型化和上下文模态类型论，Curry-Howard解释的上下文模态逻辑的连接。最后，我们将讨论如何榛子的语义本身的实现作为一个功能反应程序。我们的参考实现是使用js_of_ocaml编写的。
2019-02-04 cs.PL
The $\aleph$ Calculus
出于对布朗分子结构的可逆计算模型的需要，引入了$\aleph$演算。这种新的模型是声明性的，并发的，和基于术语的-封装在一个单一的结构中的程序数据和状态的所有信息，以满足冯诺依曼式离散计算“机器”的需要，在分子环境中的挑战。这个名字的灵感来自希腊语“不忘记”，因为强调不同变量的（可逆）学习和非学习知识。为了证明它的效用为这个目的，以及它的优雅作为一种程序设计语言，一些例子，这些例子中的两个，加法/减法和平方/平方根，配备了抽象分子实现的设计。这些例子和伴随的语法糖的自然副产品是一个完全成熟的程序设计语言alethe的设计，它也与解释器一起提供。在确定性计算机上有效地模拟$\aleph$需要在alethe解释器内对程序进行某些静态分析，以便使声明性程序顺序化。最后，工作对这样一个可逆的，声明性的计算模型的类型系统。
2021-11-30 cs.PL
A Functional Programming Language with Versions
虽然现代软件开发大量使用版本化包，但程序设计语言很少在其语义中支持版本的概念，这使得软件更新更加庞大和不安全。本文提出了一种本质上支持版本的程序设计语言。其主要目标是设计核心语言功能，以支持在一个程序中的多个版本，并建立一个适当的概念，类型安全与这些功能。所提出的核心演算称为Lambda VL，具有版本化的值，每个值在不同版本下包含不同的值。我们的类型系统的建设作为一个扩展的coeffect演算的版本映射到计算资源。类型系统保证程序存在有效的版本组合。演算使程序设计语言能够在程序中使用包的多个版本。它将作为设计高级语言功能（如模块系统和语义版本）的基础。
2021-07-15 cs.PL
Resource Usage Analysis for the Pi-Calculus
我们提出了一个基于类型的资源使用分析的-演算扩展资源创建/访问原语。资源使用分析的目标是静态地检查程序是否以有效的方式访问资源，如文件和内存。我们的类型系统是一个扩展以前的行为类型系统的演算，并可以保证安全属性，没有无效的访问被执行，以及必要的访问（如关闭操作的文件）最终执行，除非程序发散的属性。为使程序员从编写复杂类型注释的负担中解脱出来，本文还开发了一个完善的类型系统类型推断算法。基于该算法，我们已经实现了一个原型的资源使用分析器的演算。据作者所知，我们是第一个基于类型的资源使用分析，处理一个表达并发语言，如pi演算。
2006-09-13 cs.LO cs.PL
A Core Calculus for Static Latency Tracking with Placement Types
开发高效的地理分布式应用程序是一项挑战，因为程序员可以很容易地引入需要高延迟通信的计算。我们提出了一种语言设计，使延迟明确和提取类型级别的界限计算的运行时延迟。我们提出了我们的初始步骤与核心演算，使提取可证明正确的延迟界限和概述未来的工作。
2020-07-30 cs.LO cs.PL cs.SE
Modeling Quantum Computing with $π$-calculus
Constructor University Bremen Germany（不来梅_constructor大学）；REDS, School of Engineering and Management Vaud, HES-SO Yverdon-les-Bains Switzerland（沃州工程与管理学院，HES-SO）
本文提出PiQuant框架，通过扩展$\pi$-演算将量子程序建模为并发程序，变量通过通道公布状态，以提供更直观的量子计算理论模型。
2026-09-15 cs.PL
A Dependently Typed Multi-Stage Calculus
我们研究了一个多阶段的程序设计语言的依赖类型的扩展LA MetaOCaml，它支持准报价和跨阶段的持久性操作的代码片段作为第一类值和评估结构执行的程序动态生成的代码操作。依赖类型有望在多阶段编程中对动态生成的代码的行为实施强不变性--超越简单的类型安全性。然而，扩展并不是微不足道的，因为这样的类型系统必须考虑类型的阶段-粗略地说，周围引用的数量-考虑。为了严格地研究这样的扩展的性质，我们开发了$λ^{MD}$，这是Hanada和Igarashi的依赖类型的类型演算$λ^{\triangleright\%} $的扩展，并证明了它的性质，包括保存，汇合，强规范化的充分减少，和进步的分阶段减少。出于代码生成器生成的代码，其类型取决于一个值从外部的报价，我们认为跨阶段的持久性依赖类型的多阶段编程和某些类型的等价物，不直接从减少规则的意义。
2021-08-17 cs.PL
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
Strong Normalization for the Calculus of Constructions
构造演算（CC）是依赖类型编程和高阶构造性逻辑的核心理论。CC最初是在Coquand 1985年的论文中提出的，它激发了程序设计语言和类型论25年的研究。今天，CC的扩展构成了Coq和Agda等语言的基础。本综述回顾了CC强规范化属性的三个证明（良好类型的表达式不存在无限约简序列）。它突出了证明结构的相似性，同时显示了它们的差异是如何被作者的不同目标所激发的。
2022-10-07 cs.PL
pyeb: A Python Implementation of Event-B Refinement Calculus
本研究提出Event-B精化演算的Python实现工具PyEB，它将Python编写的Event-B模型转换为证明义务并通过Z3求解器验证，案例研究证实其可有效验证多种顺序算法的精化模型。
2025-04-07 cs.PL
A Pre-Expectation Calculus for Probabilistic Sensitivity
灵敏度属性描述了程序输入的变化如何影响输出，通常是通过对应输入之间距离的单调函数来上界两次运行的输出之间的距离。当程序是概率性的时，输出之间的距离就是分布之间的距离。康托洛维奇提升提供了一种通过提升底层样本空间的距离来定义分布之间距离的一般方法;通过在基空间上选择适当的距离，可以恢复其他常见的概率距离，例如全变差距离。我们开发了一个关系的预期望演算的概率程序的两次执行之间的Kantorovich距离的上限。我们通过证明机器学习算法的算法稳定性、强化学习算法的收敛性以及洗牌算法的快速混合来说明我们的方法。我们还考虑了一些扩展：证明总变差距离的下界和收敛到均匀分布。最后，我们描述了一个异步扩展我们的演算的原因对程序执行不同的控制流。
2020-08-10 cs.LO cs.PL
A Theory of RPC Calculi for Client-Server Model
使用多层程序设计语言，程序员可以指定要运行的代码的位置，以减少基于Web的客户端-服务器模型的开发工作，在基于Web的客户端-服务器模型中，程序员分别编写客户端和服务器程序，并一起测试多个程序。RPC演算是Cooper和Wadler开发的这些语言的基础之一，在程序员编写任意深度嵌套的客户-服务器的【形】交互时具有对称通信的特征。然而，现有的研究只考虑动态类型的位置。我们提出了一个类型化的RPC演算的位置跟踪类型级别。一个新的定位类型系统为客户-服务器的【形】模型的RPC演算理论铺平了道路。(In在SCP 2020和PPDP 2021上发表的以下论文中，类型化RPC演算将通过多态位置和基于类型的切片编译进行增强。）
2021-10-28 cs.PL
Behavioral Program Logic and LAGC Semantics without Continuations (Technical Report)
我们提出的行为程序逻辑（BPL），跟踪属性的动态逻辑，结合了行为类型的概念，并允许推理的非功能性的属性内的一个微积分。BPL使用行为模式[s|- τ ]，以针对行为规范τ验证语句s。行为规范概括了后置条件和行为类型。它们可用于指定其他静态分析，例如，数据流分析这使得对同一程序的多个分析结果的演绎推理成为可能，可能以不同的形式实现。我们的演算BPL验证的行为规范逐渐，常见的行为类型。这极大地简化了局部结果的规范、演算和组成。我们提出了一个面向对象的演员与期货，集成了指针分析和桥梁之间的差距行为类型和演绎验证的微积分。本技术报告介绍了（1）没有延续的核心活动对象语言（CAO）的完整LAGC语义（2）行为程序逻辑和（3）给出了行为程序逻辑中表示的行为类型的示例，方法类型。此报告包含方法类型的可靠性证明。虽然语义覆盖了带有挂起的CAO，但方法类型没有，以简化表示。
2019-04-30 cs.LO cs.PL
On the Soundness of Coroutines with Snapshots
协程是一种通用的控制流结构，可以消除事件驱动程序中固有的控制流碎片，并且在许多流行的语言中仍然缺失。带快照的协程是一个一流的、类型安全的、堆栈式的协程模型，它统一了许多可挂起计算的变体，并且足够通用，可以表达迭代器、单赋值变量、等待、参与者、事件流、回溯、对称协程和延续。在本文中，我们开发了一个正式的模型，称为$λ_{\rightsquigarrow}$（$λ_{\rightsquigarrow}$），捕获的本质类型安全，堆栈，定界的协程与快照。我们证明了标准的进步和保存安全性能。最后，我们展示了从$λ_{\rightsquigarrow}$演算到带引用的简单类型λ演算的形式化转换。
2018-06-04 cs.PL
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Deepomatic；CNRS（法国国家科学研究中心）；Université Sorbonne Paris Nord（索邦巴黎北大学）；Université de Paris（巴黎大学）
反向传播是一种经典的自动微分算法，用于计算由某类简单的一阶程序（称为计算图）指定的函数的梯度。它是多个领域的基本工具，最值得注意的是机器学习，它是有效训练（深度）神经网络的关键。近年来，一个名为可微程序设计的研究领域迅速发展，其目的是通过求助于实际的程序设计语言，赋予控制流算子和高阶组合子，如map和fold，更综合和模块化地表达计算图。在本文中，我们将反向传播算法扩展到这样的一个程序设计语言的一个范例：我们定义了一个组合程序转换从简单类型的λ演算本身增加了一个概念的线性否定，并证明了这计算梯度的源程序具有相同的效率作为一阶反向传播。转换是完全无效果的，因此提供了对反向传播动态的纯逻辑理解。
2019-11-06 cs.LG cs.LO cs.PL
Haskelite: A Tracing Interpreter Based on a Pattern-Matching Calculus
本文提出 Haskelite，一个基于模式匹配演算的 Haskell 子集追踪解释器，通过从大步语义发展小步语义，实现逐步教学解释器，并讨论实现决策与示例。
2024-07-16 cs.PL
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
我们提出了定量分离逻辑（$\mathsf{QSL}$）。与经典的分离逻辑相反，$\mathsf{QSL}$采用计算为实数的量，而不是计算为布尔值的谓词。将经典分离逻辑的连接词分离合取和分离蕴涵从谓词提升为量。这个扩展是保守的：这两个连接词是向后兼容的经典类似物，并遵守相同的法律，例如肯定前件，伴随性等。此外，我们开发了一个最弱的前提演算概率指针程序的定量推理$\mathsf{QSL}$。这种演算是Reynolds的堆操作程序的分离逻辑和Kozen/ McIver和Morgan的概率程序的最弱预期望的保守扩展。可靠性证明相对于一个基于马尔可夫决策过程的操作语义。我们的演算保留了O 'Hearn的框架规则，使本地推理。我们证明，我们的演算能够推理数量，如终止与空堆的概率，达到一定的数组排列的概率，或列表的预期长度。
2018-11-26 cs.LO cs.PL
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
我们扩展了简单类型的保护$λ$ -演算与离散概率，并赋予它一个程序逻辑的保护概率计算的关系属性的推理。这提供了一个框架的编程和推理的无限随机过程，如马尔可夫链。我们证明了逻辑的声音，解释其判断的拓扑结构的树，并通过使用概率耦合的语义分布在离散类型的关系断言。程序逻辑被设计为支持关系细化类型风格的语法导向证明，但保留了用离散分布扩展的高阶逻辑的表达能力，以及对具有不同类型或语法结构的表达式进行关系推理的能力。此外，我们的证明系统利用耦合文献中的一个著名定理来证明概率表达式的关系推理的更好的证明规则。我们用广泛的例子来说明这些好处，这些例子超出了以前系统的范围，包括随机游走之间的移位耦合和块耦合。
2018-02-27 cs.PL
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4
P4程序设计语言提供了高级的声明性抽象，将软件的灵活性带到了网络领域。不幸的是，用于在P4中表示分组数据的主要抽象，即报头类型，缺乏基本的安全保证。在过去的几年里，越来越多的程序的经验表明了不安全方法的风险，这通常会导致微妙的软件错误。本文提出了SafeP 4，可编程数据平面，其中所有的数据包数据都保证有一个明确的意义，并满足基本的安全保障，特定于域的语言。我们装备SafeP 4的正式语义和静态类型系统，静态保证头的有效性-一个共同的安全漏洞来源，根据我们对现实世界的P4程序的分析。静态地确保头的有效性是具有挑战性的，因为有效头的集合可以在运行时修改，使其成为动态程序属性。我们的类型系统通过使用一种路径敏感的推理来实现静态安全，这种推理可以跟踪来自条件语句、路由表和控制平面的动态信息。我们的评估表明，SafeP 4的类型系统可以有效地消除常见的故障，在许多现实世界的程序。
2019-06-24 cs.PL
A Gradual Probabilistic Lambda Calculus
University of Chile（智利大学）；Millennium Institute of Foundational Research on Data (IMFD)（数据基础研究千年研究所）；National University of Singapore（新加坡国立大学）
本文提出并形式化了GPLC，一种渐进源概率λ演算，通过二元概率选择运算符实现静态与动态检查的渐进过渡，支持渐进引入/移除类型和概率注解，证明了其类型安全性和渐进保证。
2026-10-16 cs.PL
Abstract interpretation as anti-refinement
本文展示了命令式程序的抽象解释和精化演算之间的对应关系：在精化演算中，程序的抽象解释是一个规范，它是一个函数。这种对应关系可以用来指导设计机械验证的静态分析，保持正确性证明以及分离的启发式部分的算法。
2014-06-13 cs.PL
A program logic for fresh name generation
我们给出了Pitts和Stark的ν-演算的程序逻辑，它是按值调用的简单类型λ-演算的扩展，具有生成新名称的机制。可以比较名字是否相等，从而产生具有细微可观察属性的程序。由生成和抽象之间的交互产生的隐藏名称通过类型上下文上的二阶量词逻辑地捕获。我们说明使用的逻辑推理著名的困难的情况下，从文献。
2021-03-12 cs.LO cs.PL
Extended Report: The Implicit Calculus
泛型编程（GP）是程序设计语言中一个日益重要的趋势。众所周知的GP机制，如类型类和C++0x概念提案，通常结合了两个特性：1）特殊类型的接口; 2）这些接口实现的隐式实例化。Scala隐式实例化是一种GP语言机制，受类型类的启发，打破了将隐式实例化与特殊类型的接口耦合的传统。相反，隐式实例化只提供隐式实例化，它被一般化为适用于任何类型。事实证明，这对于解决其他GP机制中出现的许多限制非常强大和有用。本文将隐式语言的核心思想形式化地综合到一个最小的、通用的核心演算中，称为隐式演算，并展示了如何在此基础上构建支持隐式实例化的源语言。隐式演算的一个新颖之处在于它支持部分解析和高阶规则（这一特性以前曾被提出，但从未被形式化或实现）。最终，隐式演算提供了一个形式化的隐式演算模型，语言设计者可以使用它来研究和通知在他们自己的语言中实现类似的机制。
2012-03-20 cs.PL
Towards the Safe Programming of Wireless Sensor Networks
传感器网络的部署、编程和调试是相当具有挑战性的。当前用于这些平台的程序设计语言在其规范和底层实现之间存在显著的语义差距。这一事实排除了（类型）安全应用程序的开发，这可能会简化编程和调试部署的网络的任务。在本文中，我们定义了一个核心演算编程传感器网络，并建议使用它作为一种汇编语言开发类型安全，高级程序设计语言。
2010-02-04 cs.NI cs.PL
Recovering Purity with Comonads and Capabilities
在本文中，我们采用了一种普遍有效的（ML风格的）类型λ演算，并展示了如何扩展它以允许捕获具有类型的纯表达式。我们的关键观察是，正如纯简单类型的λ演算可以扩展到支持一元类型规则的效果，不纯类型的λ演算可以扩展到支持一元类型规则的纯度。我们通过一个简单的指称模型来建立我们的类型系统的正确性，我们称之为能力空间模型。我们的模型形式化的直觉常见的系统程序员，执行效果的能力应该通过访问权限或能力进行控制，一个程序是能力安全的，如果它没有执行效果，它没有一个运行时的能力。然后，我们确定的公理范畴结构的能力空间模型验证，并使用这些公理给我们的comonadic类型系统的范畴语义。然后，我们给出了一个等式理论（替代和调用的值$β$和$η$法律）的命令λ演算，并显示其可靠性相对于此语义。最后，我们给出了一个翻译的纯简单类型的λ演算到我们的共同命令演算，并表明，任何两个条款是$βη$ -平等的STLC是平等的共同命令演算的方程理论，建立纯程序可以映射到我们的命令演算在一个方程保持的方式。
2020-11-10 cs.LO cs.PL
Dynamic Verification for File Safety of Multithreaded Programs
在本文中，我们提出了一个新的语义检查多线程程序的文件安全性。一个文件安全的程序是一个达到最终配置下提出的语义。我们用文件操作和多线程命令扩展了While语言，并将新语言称为whilef。本文证明了文件的安全性是一个不可判定的性质。在本文给出的一种特殊情况下，文件安全性成为一个可判定的属性。这种情况发生在用户提供指针信息时。如果文件是安全的，我们称之为强安全文件程序。我们修改了语言的语法和语义，并称之为SafeWhilef。
2012-06-05 cs.LO cs.PL
LNL-FPC: The Linear/Non-linear Fixpoint Calculus
本文提出LNL-FPC类型系统，混合线性和非线性递归类型，支持类型级递归，并给出基于前嵌入技术的笛卡尔范畴模型，证明其可靠且计算充分，适用于经典及量子编程等场景。
2021-04-21 cs.LO cs.PL math.CT
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
在连续随机抽样和显式递归的λ演算中，基于排序上鞅，给出了几乎必然终止的一种证明方法。这一结果在三个方面得到了推广。反音排名函数对它们必须下降的速度限制较弱，并且适用于更广泛的程序。稀疏排名函数只在程序可达状态的子集上取值，因此定义起来更简单，也更灵活。排名功能方面的替代减少战略提供了更大的灵活性，并显着增加了适用性的排名上鞅的方法来证明几乎肯定的终止，由于一个新的（限制）合流的结果，这是独立的利益。反调排序函数的概念受到McIver、Morgan、Kaminski和Katoen在一阶命令式语言中的类似工作的启发，但适用于高阶函数式语言。稀疏排名功能和合流语义扩展是唯一的高阶设置。我们的方法可以用来证明几乎肯定终止的程序，是超出了文献中的方法，包括高阶和非仿射递归。
2021-04-30 cs.LO cs.PL
CheckedCBox: Type Directed Program Partitioning with Checked C for Incremental Spatial Memory Safety
空间内存安全违规仍然是C程序的一个主要问题。Anchoked-C是一种安全的C语言方言，并扩展了它的指针类型和注释，以向后兼容的方式保证空间内存安全，允许检查指针和常规（未检查）指针类型的混合。然而，未经检查的代码漏洞可能会违反经检查的代码的空间安全保证。我们提出了一个灵活的，类型导向的程序分区机制，以masked-C，通过增强masked-C类型系统与污染的类型，使灵活的分区的程序到检查和未检查的区域，在这样的方式，未检查的区域代码不会影响空间安全检查区域。我们形式化我们的类型系统，并证明了非崩溃和非暴露性质的一个良好的类型化的PockedCBox程序。我们以一种可配置的方式实现了WebkedCBox，这使我们能够使用现有的沙箱机制（例如WebAssembly）来执行程序。因此，在这样做的过程中，通过有效地分区程序，AnchikedCBox已经防止了四个已知的漏洞。
2023-02-03 cs.CR cs.PL
