能看英文的话，PL你可能想看
Abelson和Sussman的Structure and Interpretation of Computer Programs
Sipser的Introduction to the Theory of Computation
Pierce的Types and Programming Languages
如果想做automated theorem proving就上
Harrison的Handbook of Practical Logic and Automated Reasoning
或者比较小巧可爱的Friedman和Eastlund的The Little Prover
如果想带代数玩推荐
Geddes, Czapor, Labahn的Algorithms for Computer Algebra
