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.