A Dependently Typed Multi-Stage Calculus
我们研究了一个多阶段的程序设计语言的依赖类型的扩展LA MetaOCaml，它支持准报价和跨阶段的持久性操作的代码片段作为第一类值和评估结构执行的程序动态生成的代码操作。依赖类型有望在多阶段编程中对动态生成的代码的行为实施强不变性--超越简单的类型安全性。然而，扩展并不是微不足道的，因为这样的类型系统必须考虑类型的阶段-粗略地说，周围引用的数量-考虑。为了严格地研究这样的扩展的性质，我们开发了$λ^{MD}$，这是Hanada和Igarashi的依赖类型的类型演算$λ^{\triangleright\%} $的扩展，并证明了它的性质，包括保存，汇合，强规范化的充分减少，和进步的分阶段减少。出于代码生成器生成的代码，其类型取决于一个值从外部的报价，我们认为跨阶段的持久性依赖类型的多阶段编程和某些类型的等价物，不直接从减少规则的意义。
2021-08-17 cs.PL
Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic -- Extended Version --
动态类型的面向对象语言使程序员能够编写优雅的、可重用的和可扩展的程序。然而，在当前的程序验证方法中，静态类型信息的缺失造成了显著的开销。我们的建议有两个方面：首先，我们提出了一个抽象层隐藏的复杂性动态类型时，提供了足够的类型信息。由于这本质上造成了验证静态类型程序的错觉，因此所需的工作量与静态类型的情况相当。其次，我们展示了如何所需的类型信息可以有效地获得所有类型安全的程序集成到霍尔逻辑的类型推断算法，产生一个半自动的过程，让用户专注于那些真正需要他的注意力的打字问题。虽然应用类型推断的动态类型的程序是一个行之有效的方法，现在，我们的方法补充了传统的软类型系统，除了修改程序（静态类型）和接受存在的运行时类型错误（动态类型）提供正式的证明作为第三种选择。
2015-01-12 cs.LO cs.PL cs.SE
Edit Transactions: Dynamically Scoped Change Sets for Controlled Updates in Live Programming
实时编程环境使程序员能够编辑正在运行的程序，并获得对每个单独更改的即时反馈。程序员重视活动质量，以帮助以小步骤工作，并不断添加或更正小功能，同时保持每个编辑及其运行时表现形式之间的直接联系。这种即时性可能与执行一组组合的中间步骤（例如重构）而不是在每个单独的编辑之后立即生效的期望相冲突。当一个不完整的小规模更改序列很容易破坏正在运行的程序时，这一点就变得很重要。最先进的解决方案侧重于追溯恢复机制，如调试或版本控制。相比之下，我们提出了一种主动的方法：在编辑事务中收集对程序的多个单独更改，如果认为完成，则可以使其生效。激活后，合并的步骤一起可见。编辑事务能够动态地确定范围，允许在将一组更改扩展到正在运行的应用程序之前对其进行隔离测试。这使得实时编程工作流能够完全控制更改粒度、测试的即时反馈、对正在运行的应用程序的延迟影响以及粗粒度撤销。我们在Squeak/Smalltalk中实现了编辑事务以及编辑事务感知工具。我们进行了一个案例研究，有和没有新的工具支持，比较编程活动，错误和弯路，在运行模拟实现新的功能，评估这种实现。我们的结论是，使用编辑事务的工作流有可能增加对更改的信心，减少运行时错误的可能性，并最终使实时编程更具可预测性和吸引力。
2017-04-03 cs.PL cs.SE
Performant Dynamically Typed E-Graphs in Pure Julia
本文介绍了 Metatheory.jl 第三版，通过实现高性能的 e-graphs 和 Equality Saturation 解决了高级语言元编程中的双语言问题，证明了在不牺牲与动态宿主语言直接集成舒适性的前提下，其性能可媲美 Rust 的 egg 库。
2024-06-03 cs.PL cs.SC
Monotonic References for Gradual Typing
我们描述了一种处理可变引用的替代方法（又名。指针）在逐渐类型化的语言中具有与Herman等人[2010]的先前方法不同的效率特征。特别是，我们通过静态类型代码区域中的引用降低了读写成本。我们将成本降低到与静态类型语言中的成本相同，也就是说，只是加载或存储指令的成本（对于基本数据类型）。这种成本的降低对于那些希望使用渐进类型来促进从算法的动态类型原型到静态类型的高性能实现的过渡的程序员来说尤其重要。我们心目中的程序员是科学家和工程师，他们目前在Matlab中进行原型设计，然后手动将他们的算法翻译成Fortran。我们提出了静态和动态的可变引用和类型安全的机械化证明使用伊莎贝尔证明助手的语义。
2014-07-12 cs.PL
Putting gradual types to work
在本文中，我们描述了我们的经验，将渐进类型的静态类型的函数式语言与Hindley-Milner风格的类型推断。大多数渐进类型系统的目标是在动态类型语言中改进静态检查，我们从相反的角度来处理它，并在静态类型语言中促进动态检查。我们的方法提供了一个一瞥，像SML和OCaml语言可能会处理渐进类型。我们将讨论我们的实现和面临的挑战--特别是渐进类型规则如何应用于复合和递归类型的表示。我们回顾了将动态类型添加到静态类型语言中的各种实现，以突出混合静态和动态类型的不同方式，并在保持类型系统渐进性的同时检查可能的灵感。本文还讨论了我们在语言中添加渐变类型的动机，以及在我们的工业环境中这样做的实际好处。
2021-01-28 cs.PL
Position Paper: Goals of the Luau Type System
Luau是一种脚本语言，它为Roblox平台上的用户生成体验提供支持。它是一种静态类型的语言，基于动态类型的Lua语言，具有类型推断。这些类型用于在Roblox Studio中提供编辑器帮助，Roblox Studio是用于创作Roblox体验的IDE。由于Roblox独特的异构开发人员社区，Luau必须以与传统静态类型语言不同的方式运行。在本文中，我们描述了Luau类型系统的一些目标，重点是目标与其他类型系统的目标不同之处。
2021-09-22 cs.PL
Efficient Gradual Typing
渐变类型在同一个程序中结合了静态类型和动态类型。人们希望渐进类型语言的性能介于动态类型语言和静态类型语言之间。渐进类型语言的现有实现由于与运行时强制转换相关联的开销而没有实现这个目标。Takikawa等人（2016）报告了部分类型化程序的最多100个$\times$减速。在本文中，我们提出了一个编译器，名为Grift，逐步打字评估实现技术。我们采取了一种简单但令人惊讶的未探索的实现方法来逐步类型化，即提前编译为本地汇编代码，并精心选择运行时表示和节省空间的编译器。我们的实验表明，这种方法实现的性能与OCaml的静态类型的程序和性能之间的Gambit和Racket的无类型的程序。在部分类型化的代码上，几何平均值的范围是基准测试中（未类型化）Racket的0.42 $\times$到2.36 $\times$。我们使用Siek，Thiemann，and Wadler（2015）的方法来实现类型转换。这种技术消除了所有灾难性的减速，而不会引入显著的开销。在所有基准测试中，与常规类型转换相比，转换速度从慢15%（fft）到快近2 $\times$（matmult）不等。我们还实现了Siek et al.（2015）的单调引用。单调引用消除了静态类型代码中的所有开销，对于部分类型代码，它们比代理引用快，有时高达1.48 $\times$。
2018-02-18 cs.PL
Predicting Variable Types in Dynamically Typed Programming Languages
University of Massachusetts, Amherst（马萨诸塞大学阿默斯特分校）；Department of Computer Science（计算机科学系）；Amherst（阿默斯特）；MA 01002（马萨诸塞州 01002）
动态规划语言非常流行，因为它们提高了程序员的工作效率。然而，在源代码中缺少类型使得用这些语言编写的程序难以理解，并且执行这些程序的虚拟机不能产生优化的代码。为了克服这一挑战，我们开发了一种技术来预测所有标识符的类型，包括变量和函数返回类型。我们提出了$2^{nd}$顺序内外递归神经网络的第一个实现，它有两个变体：（i）Child-Sum Tree-LSTM和（ii）可以处理大量树分支的N元RNN。我们预测的类型的所有标识符给定的抽象树，通过执行两次通过树，自底向上和自顶向下，保持内容和上下文表示的树的所有节点。这允许这些表示通过组合来自父、兄弟和子的不同路径进行交互，这对于预测类型至关重要。我们最好的模型在21个类中达到了44.33%，在我们从流行的Python基准测试中收集的Python数据集上，前三名的准确率为71.5%。
2019-01-16 cs.AI cs.PL
A prototype-based approach to object reclassification
我们调查，在功能原型为基础的语言，微积分的对象，可能会扩展自己收到一条消息，一种能力被Cardelli称为一个自我造成的操作。我们提出了一个健全的类型系统，这种演算，保证评估一个良好类型的表达式将永远不会产生一个消息未找到运行时错误。由此产生的演算是一种尝试，旨在定义一种语言，将静态类型检查的安全优势与动态类型语言中通常存在的灵活性相结合。
2018-08-13 cs.PL
Haskell's overlooked object system
Haskell提供了类型类绑定和参数多态性，而不是Java和OCaml等面向对象语言的子类型多态性。Haskell 98不带扩展、带普通扩展或带新扩展是否能完全支持传统的面向对象程序设计，包括封装、可变状态、继承、重写、静态检查、隐式和显式子类型等，这是一个有争议的问题。包括第一级词法作用域类、隐式多态类、灵活的多重继承、安全向下转换和安全协变参数。Haskell确实可以支持宽度和深度，结构和名义子类型。我们解决了保持Haskell的类型推断的特殊挑战，即使是对象和对象操作函数。面向对象特性在Haskell中作为OOHaskell库引入。OOHaskell适合作为类型化OO语言设计的沙箱。
2005-09-10 cs.PL
The Power of Types: Exploring the Impact of Type Checking on Neural Bug Detection in Dynamically Typed Languages
McGill University（麦吉尔大学）；Linköping University（林雪平大学）
本文探究类型检查对动态类型语言神经缺陷检测的影响，发现现有数据集含大量类型相关缺陷，集成类型检查器或移除训练集中类型相关缺陷可优化检测器性能。
2025-01-16 cs.LG cs.PL cs.SE
A Type System for Julia
本文针对 Julia 多重分派机制带来的组合正确性问题，提出了一种渐进类型系统，允许方法单独类型化或保持无类型，在保障类型化方法健全性的同时不牺牲脚本编写的灵活性，并引入协议机制以支持对具体实现之上的抽象进行类型化。
2023-10-25 cs.PL
A Typed Model for Dynamic Authorizations
分布式软件系统中的安全需求是动态的。在授权策略的情况下，资源意味着仅由授权方访问，但是访问资源的授权可以动态地授予/放弃。我们描述了正在进行的工作，指定通信和动态授权处理的模型。我们建立在π演算，以丰富基于通信的系统与授权规范和委托，这里授权考虑通道的使用和委托是指产生授权给另一方的行为。我们的模型包括：（i）用于授权的新颖的范围构造，其允许指定授权边界，以及（ii）用于授权的通信原语，其允许传递授权以在给定信道上动作。授权错误可能包括，例如，使用不在适当授权范围内的名称执行操作。我们引入了一个类型的纪律，确保流程永远不会减少到授权错误，即使授权是动态委托。
2016-02-11 cs.LO cs.PL
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)
本文提出一种基于受卫域论的渐近类型指称语义，结合步进索引逻辑关系的通用性与指称语义的模块化，在简单 lambda 演算上证明了 beta-eta 等式有效性与渐近性定理，并在 Guarded Cubical Agda 中完成核心定理机械化，为渐近类型程序语义提供可重用的数学基础。
2025-07-10 cs.PL
Session Types Go Dynamic or How to Verify Your Python Conversations
本文介绍了动态类型语言Python中会话类型的第一个实现。整个系统的通信安全在运行时由监视器保证，监视器检查执行跟踪是否符合相关协议。协议是用Scribble编写的，Scribble是一种基于多方会话类型的编排描述语言，添加了逻辑公式以获得更精确的行为属性。所提出的框架克服了以前的工作的局限性，所有端点的会话类型应该是静态类型的，使他们不允许与无类型的参与者的互操作性。通过用例和基准测试，展示了动态协议检测的优势、表现力和性能。
2013-12-10 cs.PL
Dynamic Program Slices Change How Developers Diagnose Gradual Run-Time Type Errors
针对渐进类型系统运行时类型错误调试困难及责备报告误导的问题，提出基于动态程序切片的TypeSlicer工具，并通过Wizard-of-Oz用户研究验证其能帮助开发者提供有效的更改建议。
2025-02-27 cs.PL
Type Checking Extracted Methods
许多面向对象的动态语言允许程序员从对象中提取方法，并将其视为函数。这允许灵活的编程模式，但对类型系统提出了挑战。特别是，一个简单的方法提取处理将要求方法在接收器类型中是逆变的，使得重写几乎是不可能的。我们提出了一个详细的调查这个问题，以及实施和评估的解决方案。方法提取是许多动态类型和渐进类型语言的特性，从Python和PHP到Flow和TypeScript。在这些语言中，可以访问作为过程记录的对象的底层表示，并且实现方法的过程可以具体化为可以独立调用的函数。在许多这些语言中，程序员可以显式地指定在调用方法实现时使用的“this”值。不幸的是，正如我们所展示的，现有的渐进类型系统（如TypeScript和Flow）在方法提取的情况下是不可靠的。键入任何这样的系统的问题是，它所允许的灵活性必须通过要求在从中提取方法的对象和稍后调用的函数值之间的连接来驯服。在Racket中，一个类似方法提取的工具，被称为“结构类型属性”，是类，泛型方法和其他API的基础，这些相同的挑战出现了，必须解决才能在Typed Racket中支持此功能。我们将展示如何结合两个现有的类型系统功能-存在类型和出现类型-产生一个健全的方法来键入方法提取。我们形式化我们的设计，扩展现有的形式化模型的类型球拍类型系统，并证明我们的扩展是健全的。我们的设计也在Racket的发布版本中实现，并且与所有现有的Typed Rack…
2021-11-19 cs.PL
Advanced Graph-Based Deep Learning for Probabilistic Type Inference
Georgia Institute of Technology（佐治亚理工学院）
诸如JavaScript和Python之类的动态类型语言已经成为使用中最流行的程序设计语言。在动态类型化程序中包含类型注释可以带来重要的好处。这种渐进类型化的方法以TypeScript编程系统为例，它允许程序员指定部分类型化的程序，然后使用静态分析来推断剩余的类型。然而，一般来说，静态类型推断的有效性是有限的，并且取决于程序结构和初始类型注释的复杂性。因此，存在对于新方法的强烈动机，所述新方法可以推进动态类型化程序中的静态预测类型的现有技术，并且以用于交互式编程环境中的可接受的性能这样做。以前的工作已经证明了使用深度学习进行概率类型推理的前景。在本文中，我们提出了过去的工作，通过引入一系列的图神经网络（GNN）模型，操作一个新的类型流图（TFG）表示。TFG将输入程序的元素表示为与语法边和数据流边连接的图节点，并且我们的GNN模型被训练来预测给定输入程序的TFG中的类型标签。我们研究了评估数据集中100种最常见类型的GNN模型的不同设计选择，并表明我们准确度最好的两种GNN配置分别达到了87.76%和86.89%的前1准确度，在过去的工作中，表现优于两种最密切相关的深度学习类型推断方法--DeepTyper，准确率为84.62%和LambdaNet，前1名的准确率为79.45%。此外，这两种配置的平均推理吞吐量分别为353.8和1，303.9文件/秒，而DeepTyper为186.…
2021-11-14 cs.LG cs.PL
Gradual Type Theory (Extended Version)
渐进类型语言被设计为同时支持动态类型和静态类型的编程风格，同时保留每种风格的优点。虽然这些语言现有的渐进类型可靠性定理旨在表明，当从完全静态设置移动到渐进设置时，基于类型的推理被保留，但这些定理并不意味着基于类型的重构和优化的正确性被保留。建立程序转换的正确性在技术上是困难的，并且在渐进式语言的元理论中经常被忽视。在本文中，我们提出了一个公理帐户的程序等价的逐步铸造演算，我们正式的逻辑，我们称之为渐进类型论（GTT）。基于Levy的按推值调用，GTT给出了按值调用和按名称调用渐进语言的公理化解释。然后，我们证明定理，证明优化和重构逐渐类型化的语言。例如，渐变类型连接词的唯一性原则表明，如果$βη$定律对连接词成立，那么连接词之间的转换必须等价于惰性转换语义。相反，这表明渴望强制转换语义违反了函数类型的可扩展性。作为另一个例子，我们表明，逐步向上的是纯粹的和对偶的，逐步向下的是严格的。我们证明了我们的理论的一致性和适用性，使用懒惰的铸造语义的实现给出了我们的类型论的逻辑关系模型，在GTT等价意味着上下文等价的程序。由于GTT也公理化了动态渐进保证，我们的模型也建立了渐进类型化的中心定理。该模型通过动态类型的实现来参数化，因此给出了一系列实现，以验证基于类型的优化和渐进保证。
2018-11-06 cs.PL
Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs
动态类型语言，如Erlang，允许开发人员快速编写程序，而无需显式提供表达式或函数定义的任何类型信息。然而，这个特性使得这些语言比静态类型语言更不可靠，因为静态类型语言中的许多运行时错误可以在编译时检测到。在本文中，我们提出了一个工具，通过使用著名的元编程和符号执行技术，可以用来执行有界验证的Erlang程序的初步工作。特别是，通过使用约束逻辑编程，我们开发了一个解释器，给出了一个Erlang程序和该程序的符号输入，返回回答约束，表示Erlang程序生成运行时错误的具体数据集。
2018-09-13 cs.LO cs.PL
Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research（西班牙国家研究委员会）
本文通过将断言属性的运行时语义集成到多变量、自顶向下、目标导向的抽象解释算法中，并利用多种推断的调用模式减少运行时检查的属性数量，从而降低开销，在Ciao系统中实现并验证了优于先前技术的性能。
2026-06-16 cs.PL
Turn: A Language for Agentic Computation
Turn Lang（Turn语言）；Prescott Data（Prescott数据）
Turn是一种用于代理计算的编译型语言，通过类型安全、能力身份系统和编译时模式吸收等机制，实现对大型语言模型推断的可靠控制和安全管理。
2026-03-07 cs.AI cs.PL cs.SE
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
针对现有编排语言缺乏节点动态决策计算执行者并传递决策的能力，提出首个具有一等进程名、支持类型与（集合）位置多态的类型化编排语言λ_{QC}，提升表达能力并验证死锁自由等特性。
2025-08-20 cs.PL
