• 提出使用定型公理和推理规则的上下文有关语法 • 讨论类型化演算的等式证明系统(公理语义)和归约系统（操作语义） • 讨论类型化演算的通用模型（指称语义）及可靠性和完备性定理 • 介绍PCF语言（递归函数留待下一章）及其公理语义和操作语义
文件格式: PPT大小: 0.98MB页数: 103
– 代数项和它们在多类别代数中的解释 – 等式规范（也叫代数规范）和等式证明系统 – 等式证明系统的可靠性和完备性（公理语义和指称语义的等价） – 代数之间的同态关系和初始代数 – 数据类型的代数理论 – 从代数规范导出的重写规则（操作语义）
文件格式: 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