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.