Post #4405122

Books on automated #ProofAssistants, like Coq, Lean, Agda, Idris, etc., fall into two groups: a vast majority aimed at working mathematicians and a handful aimed at programmers. The following is a short list of #programming-focused #books (not short tutorials) on the use of proof assistants in crafting #verified software, categorised by type theory and listed in an approximate, ascending order of sophistication: \(\textit{Coquand Calculus of Inductive Constructions}\) • Introduction to Formal Reasoning (Lean), Altenkirch • Programs and Proofs (Coq), Sergey • Functional Programming in Lean, Christiansen • Verified Functional Algorithms (Coq), Appel • Certified Programming with Dependent Types (Coq), Chlipala \(\textit{Martin-Löf Intuitionistic Type Theory}\) • Certainty by Construction (Agda), Maguire • Type-Driven Development with Idris, Brady • Verified Functional Programming in Agda, Stump • Programming Language Foundations in Agda, Wadler • Software Foundations (Idris), Pierce