cmu-15815-s15:CMU 15-815 Spring 2015

CMU 15-815 交互式定理证明 2015年Spring学期计算机科学系 课程说明 本课程介绍使用依赖类型理论证明交互式定理。 主题包括依赖数据类型、作为证明语言的类型理论、声明式与基于策略的证明风格、归纳数据类型、结构和类型类的编码、经典与构造逻辑、同伦类型理论以及细化和统一算法。 该课程将基于开发的新开源定理证明器 。 讲座 周五下午 3:30 至下午 5:00，NSH 3002。 联系信息 讲师 [教授。 Edmund M. Clarke] @cs.cmu.edu 办公室：GHC 9231 电话：(412) 268-2628 办公时间：预约 @cmu.edu 办公室：贝克大厅 161D 电话：(412) 268-8149 办公时间：预约 教学助手 @cs.cmu.edu 办公室：GHC 9232 办公时间：预约 课程秘书 夏洛特·亚诺 你... @cs.c