LCF is a deductive system for computable functions proposed by Dana Scott in 1969 in an unpublished memorandum. It has been immensely influential to the development of denotational semantics, although Scott's orinal notes have been all but lost to posterity. In 1973, Robin Milner published a seminal technical report titled “Models of LCF” in which he demonstrates the soundness of the system in a highly readable style that, in my opinion, renders the paper a must-read for any student interested in denotational semantics. The original report is available from Standard University in PDF format under the following address:
ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/73/332/CS-TR-73-332.pdf
Unfortunately, the librarians at Stanford chose to apply an undiscriminating optical character recognision to their scanned copy, which, coupled with the fact that Robin hand-wrote most of the mathematics appearing in the paper, renders the above copy all but illegible and, worse, introduces a number of subtle errors into the reasoning by confusing similarly-written symbols in a number of places.
As my personal tribute to Milner, I took some time to render his report in a modern typesetting sytem (LaTEX), taking care to preserve the original content as much as possible. The resulting PDF file is available at the following address:
http://www.jantar.org/lcf/milner73lcf.pdf
You can also download a tarball containing the actual LaTEX from which the above PDF has been constructed from the following link:
http://www.jantar.org/lcf/milner73lcf.tar.gz
Feel free to use both resources in any way you see fit, subject, of course, to the usual academic attribution practices. Also, if you spot errors or have any other comments or suggestions regarding this reprint, please do not hesitate to contact me.
Patryk Zadarnowski