EKL is a programmable interactive proof checker and constructor. It is written in MACLISP. Printed documentation is available in the manual "EKL - An Interactive Proof Checker", Stanford CS Report 1006. To run the version on SAIL, type "R EKL" to the monitor. Send any questions or bug reports to JK and JSW.