– 代数项和它们在多类别代数中的解释 – 等式规范（也叫代数规范）和等式证明系统 – 等式证明系统的可靠性和完备性（公理语义和指称语义的等价） – 代数之间的同态关系和初始代数 – 数据类型的代数理论 – 从代数规范导出的重写规则（操作语义）
文件格式: PPT大小: 856.5KB页数: 84
-λ表示法和λ演算系统概述 -类型和类型系统的扼要讨论 -基于表达式的归纳、基于证明的归纳和良基归纳
文件格式: PPT大小: 521KB页数: 34
中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第6章 递归类型
文件格式: PDF大小: 408.5KB页数: 15
中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第2章 泛代数和代数数据类型
文件格式: PDF大小: 477.37KB页数: 43
中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第1章 引言
文件格式: PDF大小: 239.9KB页数: 12
中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 04 Decision-Procedure Based Theorem Provers Tactic-Based Theorem Proving Inferring Loop Invariants
文件格式: PPT大小: 259.5KB页数: 41
中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 03 Theorem Proving for FOL Satisfiability Procedures
文件格式: PPT大小: 214KB页数: 36
中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 02 Finish Verification Condition Generation Simple Prover for FOL
文件格式: PPT大小: 217.5KB页数: 44
中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 01 Theorem Proving
文件格式: PPT大小: 174.5KB页数: 30
• 程序逻辑：描述和论证程序行为的逻辑 – Hoare逻辑 – Dijkstra最弱前条件演算 • 从程序到定理 – 验证条件生成 • 从定理到证明 – 定理证明器 – 判定过程 • 循环不变式的推断 • 以George C. Necula教授的讲稿为主来介绍
文件格式: PPT大小: 306.5KB页数: 32