Report Number: CS-TR-72-288
Institution: Stanford University, Department of Computer Science
Title: Logic for Computable Functions: description of a machine implementation.
Author: Milner, Robin
Date: May 1972
Abstract: This paper is primarily a user's manual for LCF, a proof-checking program for a logic of computable functions proposed by Dana Scott in 1969 but unpublished by him. We use 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. The user's task is alleviated by two features: a subgoaling facility and a powerful simplification mechanism. Applications include proofs of program correctness and in particular of compiler correctness; these applications are not discussed herein, but are illustrated in the papers referenced in this introduction.
http://i.stanford.edu/pub/cstr/reports/cs/tr/72/288/CS-TR-72-288.pdf