CCF软件大会2026|编程语言前沿技术论坛

一、论坛介绍

编程语言前沿技术论坛聚焦编程语言、编译器、程序分析和验证等领域的最新理论和技术成果，论坛将邀请来自学术界及产业界专家，通过分享最新研究与实践的进展，帮助编程语言领域的广大学术研究者及开发者了解、学习和交流最前沿的编程语言理论和技术。欢迎计算机科学、软件工程、编译器与编程语言等相关学科专家和学者前来参加。

二、论坛组织委员会

• 陈俊洁（天津大学）
• 冯新宇（南京大学）
• 贺飞（清华大学）

三、论坛安排

日程安排：

时间：2026年11月6日，9:00~12:00

地点：天津市社会山国际会议中心酒店，三层接见厅

论坛议程：

四、论坛报告嘉宾简介

1. 王戟 教授

题目：安全编程语言Trust C若干进展

摘要：本报告将安全编程语言视为程序构造与形式验证的统一载体，将安全编程可信保证梳理为三种主要模式：语言内生的自动保证、规约驱动的自动验证、显式证明构造与交互式定理证明。以此为基础，介绍安全编程语言Trust C的若干进展：它是基于C的渐进式安全编程语言；安全保证思路是利用内生机制排除普遍且可结构化的错误、规约驱动验证处理程序特定要求、显式证明构造承担功能正确和功能安全的语义论证；这些安全保证内嵌于Trust C的验译器之中，并通过其IDE与外部分析、验证工具和AI辅助工具集成。

简介：王戟，国防科技大学教授，复杂关键软件环境全国重点实验室副主任，中国计算机学会会士。从事可信、智能与新兴软件技术研究，在复杂关键软件高可信保证、神经符号融合系统、虚拟计算环境等方面取得了重要进展，在国家和国防重大重点工程发挥了重要作用。获国家和省部级奖励6项，发表论文200余篇。曾获国务院政府特殊津贴、国家杰出青年科学基金、教育部长江学者特聘教授。历任中国计算机学会理事、形式化方法专委主任、软件工程专委副主任。

2. 王迪 助理教授

题目：大模型时代的编程语言设计初探

摘要：大模型正在成为代码的作者，如何检查其生成程序的正确性，成为编程语言设计的重要问题。本报告从表达能力与可检查性的关系回顾编程语言的演化，讨论作者角色的变化如何推动语言设计转向"大模型可生成、机器可检查"的协同目标：由人明确意图、审查规约，大模型生成实现与证明，机器检查实现是否满足规约。围绕这一目标，报告介绍面向系统软件的C*语言探索：沿用C的语法编写实现与证明，将实现、规约和证明就近组织在同一份源码中，通过符号执行与证明执行交替推进验证，并为智能体提供增量检查与状态反馈。这些设计将语言的熟悉度、推理的局部性和检查的及时性结合起来，探索开发与证明一体化的编程方式。

简介：王迪是北京大学计算机学院的助理教授。他于2022年在美国卡内基梅隆大学获得博士学位，于2017年在北京大学获得学士学位。他的研究兴趣包括形式化验证、程序分析、类型系统以及概率编程，目前的研究项目涉及资源安全的系统编程、可编程贝叶斯推断、量化程序分析以及面向证明的编程语言。他获得了国家优秀青年科学基金项目（海外）资助，多项研究成果发表于编程语言领域的顶级会议POPL、PLDI、OOPSLA、ICFP等。他是中国计算机学会形式化方法专委会执行委员。

3. 傅荣枭 高级工程师

题目：仓颉编程语言 Modal Type 特性简介

摘要：基于类型系统提供的静态约束改善程序安全性与提升运行性能，一直是学术界与工业界共同关注和探索的重要方向。本次报告将会介绍在仓颉编程语言中的 Modal Type 特性的设计和工程实践的进展。为了更高效的内存管理，更精细安全的资源管理，以及更安全的并发等目标，我们参考 OxCaml 等现有工作，在仓颉编程语言中引入了 Modal Type 特性。此特性作为对仓颉现有类型系统的增强，允许使用附加在数据类型上的 Mode 标记表示使用该类型的对象时会受到的一系列约束，并在此基础上提供相应的保证或执行相关的优化。当前我们的设计涵盖了用于约束对象生命周期的 Local Mode，用于表达所有权的 Unique Mode，以及用于控制可变性的 Immutable Mode。同时，本次报告将结合典型应用场景，探讨 Local Mode 在降低内存峰值、减少 GC 压力等方面的应用价值。

简介：傅荣枭，华为编程语言实验室高级工程师。电子科技大学与格拉斯哥大学本科毕业，爱丁堡大学硕士与博士毕业。研究方向包括编程语言设计，类型系统等。目前主要关注仓颉编程语言的语言设计。

4. 谭添 助理教授

题目：骑河：面向硬件的通用型静态分析框架

摘要：静态程序分析是公认提升软件质量的有效技术，可支撑软件缺陷检测、安全分析与程序理解等复杂任务。其中，通用型静态分析框架是各类先进软件分析技术的关键基座，能显著降低新分析的研发门槛。然而在硬件设计领域，尽管同样使用程序设计语言（Verilog等）进行开发，但硬件静态分析技术尚未得到充分发展和应用。针对这一问题，我们认为长期缺乏通用型硬件静态分析框架是限制该领域发展的主要原因之一。但面向硬件构建此类框架极具挑战：一方面，硬件静态分析并非软件分析技术的简单移植，而需针对硬件固有的并发语义、寄存器同步机制和位向量运算等特性进行专门设计；另一方面，硬件领域缺乏可参考的通用框架先例，针对硬件设计语言，通用型静态分析框架应提供哪些功能以支撑分析硬件分析技术的研发与应用，本身也是我们需要探索的问题。为挖掘硬件静态分析技术的潜力，我们设计并实现了国际首个通用型 Verilog 静态分析框架"骑河"。该框架代码规模超过 10 万行，现已连同配套文档一并开源发布。本报告将介绍骑河面向硬件特性的框架设计，并展示基于该框架在硬件缺陷检测、硬件安全分析和硬件设计理解三类应用上的初步探索。实验结果验证了静态分析技术在硬件设计领域的有效性，展现出良好的应用前景；同时，骑河也显著降低了相关分析应用的开发成本。

简介：谭添，南京大学计算机学院助理教授，博士生导师。2017年博士毕业于澳大利亚新南威尔士大学，2017至2019年于丹麦奥胡斯大学从事博士后研究工作。研究方向为程序分析与程序设计语言。研究成果发表在TOPLAS、PLDI、POPL、OOPSLA、TOSEM、TSE、ICSE、FSE、ISSTA等相关领域的重要国际期刊与会议。曾获NASAC青年软件创新奖（2024）、ICSE 2025最佳软件制品奖、ICSE 2025 杰出论文奖、OOPSLA 2023杰出软件制品奖、ECOOP 2016杰出论文奖等奖项。主导设计并开发程序分析框架"太阿"。

5. 叶文佳 高级副研究员

题目：Typed and Staged Tile-Based GPU Programming

摘要：High-performance GPU programming today relies heavily on Python-based meta-programming systems like TileLang and Triton. These systems offer flexibility by allowing users to programmatically generate intermediate representations (IR) for the GPU. However, this flexibility comes at a cost: the meta-logic—defining layouts, schedules, and tile sizes—is opaque to the compiler, residing in a dynamic runtime environment (Python) rather than the static type system. Errors in kernel configuration are often detected late, and cross-stage optimizations are missed. In this talk, we argue for a new class of GPU Domain Specific Languages (DSLs) that incorporate static meta-programming features directly into the surface language. Drawing on the success of the P4 programming language in networking, we propose lifting GPU memory hierarchy concepts—such as layouts and tile sizes—into a dependent type system, supported by first-class multi-stage programming primitives. This approach preserves the generative power of Python while enabling compile-time verification and deep, whole-program optimization.

简介：叶文佳主要从事程序语言理论、类型系统与形式化方法研究，重点关注渐进类型理论及其在高可信软件系统中的应用。曾在新加坡国立大学从事博士后研究，后任英国布里斯托大学高级副研究员。近五年以唯一第一作者发表多篇CORE A类论文，研究成果发表于PLDI、OOPSLA、TOPLAS等国际顶级会议和期刊，成果荣获PLDI杰出论文奖。相关研究成果已应用于微软Koka编程语言。未来将聚焦高可信AI编译器的渐进式语义与类型方法，致力于提升人工智能基础软件的可靠性与安全性。

6. 栾晓坤 Research Fellow

题目：从证明失效到可信修复：形式化证明维护的分析与自动化

摘要：随着形式化验证技术的发展和应用，形式化证明代码与证明库的规模不断增长，相应的维护需求也日益增加。证明器版本、依赖库及上下文环境的演化，可能使原本有效的证明失效，即使待证命题本身并未改变。如何理解这些失效，并高效、可信地完成修复，成为证明工程中的重要问题。本报告以 Isabelle 证明器及 Archive of Formal Proofs（AFP）的真实版本演化为背景，分析证明兼容性问题的典型表现、根本原因和常见修复方式，并讨论相关发现对证明开发与维护的启示。在此基础上，进一步探讨如何结合大语言模型与交互式证明工具自动修复失效的证明，如何构建贴近真实维护场景的评测基准，以及如何通过独立验证与证明信任检查，确保修复结果的有效性与可信性。最后，讨论 AI 辅助形式化证明维护面临的挑战与机遇。

简介：栾晓坤，新加坡国立大学计算机学院研究员，博士毕业于北京大学应用数学专业。主要从事可信人工智能与形式化方法的交叉研究，重点关注 AI 智能体的可靠性与安全性、人工智能辅助形式化推理，以及形式化证明的自动化与维护。研究成果发表于 FSE、ICSE、POPL、NDSS、ICML、ICLR 等国际学术会议，曾获 ACM SIGSOFT 杰出论文奖（FSE 2025）和最佳论文奖（ICFEM 2025）。

五、论坛组织委员会简介

1. 陈俊洁 教授

简介：陈俊洁，天津大学教授、博导、软件学院副院长，软件工程团队(TJU-WISE Lab)负责人，主持国家优青、重点研发计划青年科学家等项目；博士毕业于北京大学；研究方向主要为基础软件质量保障、代码智能体等；入选中国科协青年人才托举工程、斯坦福大学发布的全球前2%顶尖科学家榜单，荣获CCF优博、电子学会自然科学一等奖、十项最佳/杰出论文奖等奖项；成果在华为、字节等多家知名企业落地；担任CCF系统软件专委常委，AUSE、FCS、JCST、JSEP等期刊编委/青年编委，ICSE、FSE、ASE、ISSTA等顶会PC。

2. 冯新宇 教授

简介：冯新宇，南京大学教授，华为编程语言首席专家，仓颉编程语言首席架构师。主要研究方向为程序设计语言的设计与实现、程序设计语言理论、以及形式化程序验证。主要工作包括仓颉编程语言、安全系统编程、操作系统内核验证、编译器验证、以及细粒度/无锁并发算法验证等。

3. 贺飞 副教授

简介：贺飞，清华大学长聘副教授、博士生导师，软件系统与工程研究所所长。长期从事程序验证、模型检验与自动推理研究，在程序终止性证明、并发程序验证及面向验证的SMT理论方面取得成果。开发的程序验证工具四次获国际软件验证大赛并发安全赛道冠军。发表论文百余篇，入选国家特支计划青年人才，获"中创软件人才奖"。