I realise this is slightly off topic, but I am keen to find out what `types people' use for teaching logic to computing undergraduates. In particular, I am looking for feedback on systems which allow students to build proofs (preferably in a natural deduction style) in propositional and predicate logic. The best thing would be to reply directly to me, and I will post a summary of responses to the types list. Thanks very much, Simon Thompson