定理证明器 Coq 与机械语义研究

• 作者: 刘强 杨宗源 窦亮
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 定理证明 形式语义 Lambda演算 机械语义
• 年，卷（期）: 2015,（10）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 10-14
• 页数: 5页
• 分类号: TP301
• 字数: 7102字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2015.10.003

摘要

随着证明理论和定理证明器的不断发展与成熟，形式语义研究已经从传统的基于手工证明的研究进入到机器可处理的机械语义的研究。交互式定理证明器 Coq 具备强大的描述能力，可以形式化地描述程序语法和语义，利用其内置函数式编程语言实现对程序语义的复杂操作，通过其证明系统形式地证明操作的正确性。根据形式语义的理论，针对简单类型 Lambda 演算的操作语义和指称语义，展示了如何利用定理证明器 Coq 的归纳定义实现它们的形式描述，并对语义的重要属性进行证明，表明机械语义是确保基础软件正确性的基础。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨宗源	华东师范大学计算机科学技术系	32	326	9.0	17.0
2	窦亮	华东师范大学计算机科学技术系	10	73	5.0	8.0
3	刘强	华东师范大学计算机科学技术系	3	1	1.0	1.0