The project EKL at Stanford Artificial Intelligence Laboratory was initiated by Jussi Ketonen and John McCarthy at the beginning of the 1980s, building on the experience of Richard Weyhrauch's theorem prover FOL. EKL is a LISP program, designed for an efficient representation of mathematical proofs and for a versatile use in program verifiaction. Features of EKL are:

EKL was written around 1980. From 1980 to 1984 EKL was used in the following projects:

Further documentation on EKL:

back home