Type Theory and Formal Proof

目录:

• 无类型lambda演算(Untyped lambda calculus)
  • lambda-项(lambda-terms)
  • 自由变量,约束变量和绑定变量(Free variables,bound variables and binding variables)
  • Alpha 转换 (Alpha conversion)
  • 替换(Substitution)
  • Lambda-项 模 alpha-等价 (lambda-terms modulo alpha-equivalence)
  • Beta-归约 (Beta reduction)
  • 范式与合流性(Normal forms and confluence)
  • 不动点理论 (Fixed Point Theorem)
• 简单类型的lambda演算(Simple typed lambda calculus)
  • 简单类型(simple types)
  • Church 定型 与 Curry 定型 (Church-typing and Curry-typing)
  • Church \(\lambda\rightarrow\)的派生规则(Derivation rules for Church’s \(\lambda\rightarrow\))
  • 派生的不同格式(Different formats for a derivation in \(\lambda \rightarrow\))
  • 类型论中需要解决的几类问题(Kinds of problems to be solved in type theory)
  • \(\lambda\rightarrow\)的性质(General properties of \(\lambda\rightarrow\))
  • 归约与\(\lambda\rightarrow\)(Reduction and \(\lambda\rightarrow\))
  • 总结