paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A tale of intersection types

交集类型的故事
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 该论文是交集类型与形式语义的综述，属于程序语言理论中与静态分析和形式验证有间接关联的基础方向，但不涉及用户核心关注的 LLM/Agent、机器学习系统、浮点程序分析或贝叶斯程序分析，也 lacks 问题驱动与工业落地。引用 8 inbox
Viviana Bono, Mariangiola Dezani-Ciancaglini
类型系统形式语义
crossref: 2026-09-12

AI 速览

一句话：综述交集类型自 20 世纪 70 年代以来的发展及其在语义、验证、综合与语言表达力等方面的应用。

本文是对交集类型（intersection types）的轻量综述。交集类型自 20 世纪 70 年代提出以来，已从一种类型构造发展为具有广泛应用的语义与程序分析工具。文章回顾其基本思想与发展脉络，并概述若干代表性应用：刻画 λ-项与 π-演算进程的行为，构造 λ-模型，验证高阶程序性质，合成代码，以及增强编程语言的表达力。作为一篇导览性文章，它不追求技术细节的完整覆盖，而是勾勒交集类型在类型论、形式语义、程序验证与程序合成等方向的联系与影响，为读者提供进入该领域的路线图。

问题
交集类型自 20 世纪 70 年代提出后应用广泛，但需要一篇概览来梳理其发展脉络与主要应用。
方法
以轻量综述形式回顾交集类型的基本思想，并列举其在语义、验证、合成和语言表达力等方面的代表性应用。
评估
作为导览性文章，通过文献综述与概念梳理而非实验评估来呈现交集类型的影响。
原文摘要（Abstract）

Intersection types have come a long way since their introduction in the Seventies. They have been exploited for characterising behaviours of λ-terms and π-calculus processes, building λ-models, verifying properties of higher-order programs, synthesising code, and enriching the expressivity of programming languages. This paper is a light overview of intersection types and some of their applications.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5529,
  title = {A tale of intersection types},
  author = {Viviana Bono and Mariangiola Dezani-Ciancaglini},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394733}
}