The language of an interactive proof checker
Jussi Ketonen, Joseph S. Weening · 1983
We describe the underlying language for EKL, an interactive theorem-proving system currently under development at the Stanford Artificial Intelligence Laboratory. Some of the reasons for its development as well as its mathematical properties are discussed.