Student Programming Projects

[Albert Lai]

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 http://www.cs.utoronto.ca/~trebla/fp/prover/index.html

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.