paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Special issue on Programming with Dependent Types Editorial

依赖类型编程专刊导言
JFP vol.272017匹配度 2/10 · 这篇论文是依赖类型编程特刊的导言，主题集中在依赖类型、证明助手与证明工程的基础与发展，仅与形式化验证有较远的领域关联；它不涉及 LLM/Agent 改进静态分析或形式化验证，也不涉及浮点程序分析、贝叶斯程序分析或 Agentic 程序分析等用户核心方向。引用 1 inbox
WOUTER SWIERSTRA, PETER DYBJER
类型系统定理证明与证明工程
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话：本期特刊导言回顾依赖类型编程的基础与发展，并介绍收录的六篇覆盖广泛主题的论文。

近年来，带依赖类型的函数式编程语言持续受到关注。依赖类型编程的基础可追溯至 20 世纪 70 年代 Martin-Löf 的工作。过去几十年间，这一构想催生了基于依赖类型的证明助手与函数式编程语言，Agda、Coq、Idris 等系统的日益流行反映出该研究领域不断增长的势头。本期特刊在 2015 年 10 月首次发出征稿后，最终接收六篇文章，覆盖从理论到实践的广泛主题。该导言概述了这一研究方向的渊源与现状，并引出专刊中六篇论文所代表的多样的研究议题，为读者了解依赖类型编程领域的最新进展提供了入口。

问题
依赖类型编程语言与证明助手经过数十年发展已形成活跃研究领域，但需要对其基础、现状与多样化研究方向进行阶段性梳理与集中展示。
方法
通过组织专刊征稿，汇集六篇覆盖广泛主题的论文，并在导言中回顾依赖类型编程从 Martin-Löf 工作到现代系统的发展脉络。
评估
以收录论文的主题覆盖面体现该领域的研究广度，并借助 Agda、Coq、Idris 等系统的流行度说明该方向的持续增长势头。
原文摘要（Abstract）

There has been sustained interest in functional programming languages with dependent types in recent years. The foundations of dependently typed programming can be traced back to Martin–Löf's work in the 1970s. In the past decades, this vision has given rise to the development of proof assistants and functional programming languages based on dependent types. The increased popularity of systems such as Agda, Coq, Idris, and many others, reflects the growing momentum in this research area. After sending out our first call for papers in October 2015, we are happy to accept six articles in this special issue covering a wide spectrum of topics.

链接与引用

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

BibTeX 
@article{SwierstraD17,
  title = {Special issue on Programming with Dependent Types Editorial},
  author = {WOUTER SWIERSTRA and PETER DYBJER},
  journal = {Journal of Functional Programming},
  volume = {27},
  year = {2017},
  doi = {10.1017/s0956796817000065}
}