PL相关

[wangwangwar]

http://www.ccs.neu.edu/home/matthias/HtDP2e/index.html http://cs.brown.edu/courses/cs173/2012/book/ http://www.eopl3.com/

[wangwangwar]

强类型语言如Haskell可以利用类型来建模一部分逻辑，然后利用编译器来辅助证明。而Dependent Type语言更强化了这一块。 有些自动证明的语言，coq。