paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A spectrum of type soundness and performance

类型健全性与性能的谱系
ICFP 2(ICFP)2018匹配度 2/10 · 该论文属于类型系统与形式语义方向,讨论渐进类型的健全性语义与性能比较,不涉及 LLM/Agent、面向机器学习或 Agentic 程序的静态分析、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 30 inbox
Ben Greenman, Matthias Felleisen
crossref: 2026-09-10

AI 速览

一句话:提出统一语义框架解释渐进类型中三种类型健全性方法,并系统比较其性能。

渐进类型的文献对混合静态与动态类型代码的程序健全性提出了三种根本不同的处理方式。本文提出一个统一的语义框架,将这三类方法纳入同一形式化体系,并解释它们各自的语义差异。论文进一步说明每种方法如何影响开发者的实际编程工作,例如错误检测时机与责任归属。最后,作者在一个实现平台上对三种方法进行系统性的性能比较,揭示健全性策略与运行时开销之间的权衡关系。

问题
渐进类型中,混合静态与动态类型程序的类型健全性存在三种根本不同的定义方式,缺乏统一理解。
方法
提出一个统一的语义框架,将三种类型健全性方法形式化,并分析各自对开发者工作的影响。
评估
在单一实现平台上对三种类型健全性方法进行系统性的性能比较。
原文摘要(Abstract)

The literature on gradual typing presents three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. This paper presents a uniform semantic framework that explains all three approaches, illustrates how each approach affects a developer's work, and adds a systematic performance comparison for a single implementation platform.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot280,
  title = {A spectrum of type soundness and performance},
  author = {Ben Greenman and Matthias Felleisen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
  year = {2018},
  doi = {10.1145/3236766}
}