Comment by foopdoopfoop

https://softwarefoundations.cis.upenn.edu/ is a nice introduction to computational logic, interactive theorem provers, lambda calculus, and the power of type systems.