Report Number: CS-TR-74-446
Institution: Stanford University, Department of Computer Science
Title: LCFsmall: an implementation of LCF.
Author: Aiello, Luigia
Author: Weyhrauch, Richard W.
Date: August 1974
Abstract: This is a report on a computer program implementing a simplified version of LCF. It is written (with minor exceptions) entirely in pure LISP and has none of the user oriented features of the implementation described by Milner. We attempt to represent directly in code the metamathematical notions necessary to describe LCF. We hope that the code is simple enough and the metamathematics is clear enough so that properties of this particular program (e.g. its correctness) can eventually be proved. The program is reproduced in full.
http://i.stanford.edu/pub/cstr/reports/cs/tr/74/446/CS-TR-74-446.pdf