Logic for Computable Functions Description of a Machine Implementation,

摘要

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. (Modified author abstract)