6月6日上午，南京航空航天大学陈钢教授应邀做客三元名家论坛，为师生作题为“Pella：一个带类型的高层硬件描述语言”的专题讲座，院长童向荣教授、科研骨干教师及在校研究生共同参与。

讲座中，陈钢教授介绍Pella——一个嵌入Coq定理证明器的硬件描述基础设施。Pella的核心创新是使用依赖类型将位宽、索引边界和控制流完整性直接编码到类型签名中，实现“错误前移”（Error Front-Loading）：将错误捕获从仿真/综合阶段提前到编译期。陈钢教授特别强调了Pella在AI时代的战略价值：当代码主要由大语言模型生成时，设计工作的核心挑战不再是编写代码本身，而是（1）做出一个全面可靠的高层描述；（2）验证设计的正确性。Pella作为“规范-验证-生成”工作流中的类型安全中间层，为AI辅助大规模硬件设计提供了可行的技术路径。报告面向软件领域的研究者和教师，无需任何硬件设计或 Coq 使用经验，从零开始构建必要的背景知识。

在互动环节，现场师生与陈钢教授就相关技术细节与应用前景进行了热烈讨论。本次讲座为师生们带来了前沿的学术视角，拓宽了科研思路。学院表示将继续举办高水平学术活动，营造浓厚创新学术氛围。

专家简介：

陈钢，国家特聘专家，中国计算机学会杰出会员，巴黎第七大学博士（程序语言专业），曾在澳大利亚和美国的EDA公司和大学工作，2013年入选国家特聘专家，并在北京京航计算与通讯研究所工作，2018年起任南京航空航天大学计算机科学与技术学院教授。在南京航空航天大学组建形式化工程数学团队。开展形式化工程数学，人工智能，EDA和程序语言设计方面的研究工作。开发了嵌入在Coq中的带类型硬件描述语言Pella；带类型学习框架和基于重写的AI编译系统Ionia，带类型量子计算编程语言和形式化量子程序验证系统Chalcis，增量式Verilog语言语法分析和前端工具Stagira等软件项目。开发了多个AI智能助手。发表了60多篇论文，6项授权专利。

作者：郑强   责任编辑：马文明   审核：段昕