Background : computational structures
Samson Abramsky, Dov M. Gabbay, T. S. E. Maibaum · Clarendon Press eBooks · 1992
J.W. Klop: Term rewriting systems H.P. Barendregt: Lambda calculi with types D.M. Gabbay: Elements of algorithmic proof Lawrence C. Paulson: Designing a theorem prover Colin Stirling: Modal and temporal logics.