The author uses the name LCF also for the logic itself, which is presented at the start of the paper, The proof-checking program is designed to allow the user interactively to generate formal proofs about computable functions and functionals over a variety of domains, including those of interest to the computer scientist - for example integers, lists and computer programs and their semantics.