Sequent Calculus in HaskellA Theorem Prover for Intuitionistic Propositional Logic One of the standard textbooks for ML, the "other" functional programming language, is Paulson's ML for the Working Programmer. Some years back, this is the book that I first learnt functional programming from. The book culminates in a theorem prover for classical first order logic, which is the kind of task that functional programming languag
