Mario Aiello Artificial Intelligence Laboratory, Stanford University, California and Istituto di Scienze dell'lnformazione, Universita'di Pisa, Italy i. Introduction LCF (Logic for Computable Functions) is an interactive proof-checker. It is based on a logic (proposed in an unpublished report by D. Scott) where facts about computable functions are expressible and in which a powerful induction principle (allowing to prove properties about recursively defined functions) holds. This logic has been augmented in the implementation of LCF by:

1) a simplification mechanism, 2) the possibility of creating ti~ eorems, which can thereafter be used as lemmas, 3) a goal structure with a subgoaling mechanism.

LCF is described in Milner (i 972a)(actually the user's manual), Milner (1972b), Milner and Weyhrauch (1972), Weyhrauch and Milner (1972). Here we can't enter into details about it, we want only to point out its main applications. Milner and Weyhrauch (1972) worked out, in LCF, the proof of the correctness of the compiler for a simple programming language and Weyhrauch and Milner (] 972) proved the correctness of a program for the computation of the factorial function. This program is written in a programming language in which the basic instructions of input, output and assignment are expressible as well as the three basic types of" decomposition"(see Dijkstra (1972)), ie concatenation, selection and WHILE-repetition. The syntax and the semantics of this