Herbert Stoyan. The History of Lisp. 1980. Updated in the 1990s, translated into English 2023.

Includes a history of the route from PLANNER to CONNIVER, in which the former was criticised for being a theorem prover when a programming language was needed – an argument between two schools that’s still going on today, as seen in the emergence of Lean.