Student Programming Projects

Albert Lai
21 Sep 2001 00:30:56 -0400

Consider goal-directed theorem prover (or proof checker).  Two existing
samples are in Lawrence Paulson's ML for the Working Programmer, and
yours truly's

The advantage of mine is it illustrates monads.  The advantage of Paulson's
is it doesn't scare people with monads :) and it includes a substitution
library (yet another monad, but shhh) for use in first-order logic.